Changeset 3633


Ignore:
Timestamp:
Mar 8, 2017, 10:45:04 AM (4 months ago)
Author:
mulligan
Message:

Fleshed out first part of introduction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/jar-cerco-2017/introduction.tex

    r3620 r3633  
    1212\label{sect.introduction}
    1313
    14 %\paragraph{Problem statement.}
    15 Programs can be specified using both functional constraints (what the program
    16 must do) and non-functional constraints (what time, space or other resources
    17 the program can use).  At the current state of the art, functional properties
    18 are verified by combining user annotations---preconditions, invariants, and so
    19 on---with a multitude of automated analyses---invariant generators, type
    20 systems, abstract interpretation, theorem proving, and so on---on the
    21 high-level source code of the program.
    22 
    23 By contrast, many non-functional properties are verified by analysing the
    24 low-level object code. Analysis on low-level object code has several problems,
    25 however:
     14Programs are specified using both functional and non-functional constraints.
     15Functional constraints dictate what tasks a program must do; non-functional constraints limit the resources the program may consume whilst completing those tasks.
     16Depending on the application domain, non-functional constraints are as important as functional constraints when specifying a program.
     17Real-time systems, with hard limits on application response times, and implementations of cryptographic primitives, which must be hardened to timing side-channel attacks, are two examples that fit this pattern.
     18A cryptography library susceptible to a timing side-channel attack is not an annoyance---it's an implementation error that undermines the entire purpose of the library.
     19
     20Currently, a program's functional properties can be established by combining user annotations---preconditions, invariants, and so on---with various automated and semi-automated analyses---invariant generators, type systems, abstract interpretations, applications of theorem proving, and so on---on the high-level source code of the program.
     21Functional properties of a program are therefore established by reasoning about the source code that the application programmer actually sees.
     22Further, the results of any analysis can be communicated to the programmer in terms of abstractions, control flow, and an overall system design that they are familiar with.
     23
     24By contrast, a program's non-functional properties are established by reasoning on low-level object code produced not by a programmer, but by a compiler.
     25Whilst analyses operating at this level can and do produce very accurate results, analysis at such a low-level of abstraction invariably has disadvantages:
    2626
    2727\begin{itemize*}
    2828\item
    29 It can be hard to deduce the high-level structure of the program after compiler
    30 optimisations. The object code produced by an optimising compiler may have a
    31 radically different control flow to the original source code program.
    32 \item
    33 Techniques that operate on object code are not useful early in the development
    34 process of a program, yet problems with the design or implementation of a
    35 program are cheaper to resolve early in the development process.
    36 \item
    37 Parametric cost analysis is very hard: how can we translate a cost that depends
    38 on the execution state, for example the value of a register or a carry bit, to
    39 a cost that the user can understand while looking at the source code?
    40 \item
    41 Performing functional analysis on object code makes it hard for the programmer
    42 to provide information about the program and its expected execution, leading to
    43 a loss of precision in the resulting analysis.
     29It can be hard to deduce the high-level structure of the program after compiler optimisations.
     30The object code produced by an optimising compiler may have a radically different control flow to the original source code program.
     31\item
     32Object-code analysis is unstable.
     33Modern compilers and linkers are highly non-compositional: they implement a variety of sophisticated optimisation passes, and use an abundance of procedural, intra-procedural, module-level, and link-time analyses to direct these optimisations.
     34As a result, small changes in high-level source code can produce radically different object code outputs from a compiler, affecting any analysis effected on that object code.
     35\item
     36It is well understood by Software Engineers that problems with the design or implementation of a program are cheaper to resolve early in the development process. %cite
     37Despite this, techniques that operate on object code are not useful early in the development process of a program, where programs may be incomplete, with missing functionality, or entire subcomponents missing.
     38\item
     39Parametric cost analysis is very hard: how can we translate a cost that depends on the execution state, for example the value of a register or a carry bit, to a cost that the user can understand whilst looking at the source code?
     40\item
     41Performing functional analysis on object code makes it hard for the programmer to provide information about the program and its expected execution, leading to a loss of precision in the resulting analysis.
     42It is hard for the programmer to understand the results of the analysis, or direct its execution, as high-level abstractions, control flow constructs, and so on, introduced by the programmer are `translated away'.
    4443\end{itemize*}
    4544
Note: See TracChangeset for help on using the changeset viewer.