Changeset 3644


Ignore:
Timestamp:
Mar 8, 2017, 5:07:52 PM (8 months ago)
Author:
mulligan
Message:

intro finished?

File:
1 edited

Legend:

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

    r3643 r3644  
    270270}
    271271\end{lstlisting}
    272 \caption{The instrumented version of the program in Figure~\ref{test1},  with instrumentation added by the CerCo compiler in red and cost invariants added by the CerCo Frama-C plugin in blue.
    273 The \lstinline'__cost', \lstinline'__stack' and \lstinline'__stack_max' variables hold the elapsed time in clock cycles and the current and maximum stack usage. Their initial values
    274 hold the clock cycles spent in initialising the global data before calling
    275 \lstinline'main' and the space required by global data (and thus unavailable for
    276 the stack).
     272\caption{The C program in Figure~\ref{test1} embellished with instrumentation added by the CerCo compiler in red and cost invariants added by the CerCo Frama-C plugin in blue.
     273The \lstinline'__cost', \lstinline'__stack' and \lstinline'__stack_max' global variables hold the elapsed time in clock cycles and the current and maximum stack usage.
     274Their initial values hold the clock cycles spent initialising global data in the preamble before calling \lstinline'main' and the space required by global data (and thus unavailable for the stack).
    277275}
    278276\label{itest1}
    279277\end{figure}
    280278
    281 How should a Software Engineer use our tool in anger?
    282 We illustrate an example C program on the left in Figure~\ref{test1}, and a prospective workflow making use of our toolset on the right of Figure~\ref{test1}.
     279How should a Software Engineer use the CerCo toolset in anger?
     280We provide an illustrative C program on the left of Figure~\ref{test1}, along with a prospective workflow making use of our toolset on the right of Figure~\ref{test1}.
    283281An engineer writes their C program and feeds it as input to the CerCo compiler, which outputs an instrumented version of the same program that updates fresh global variables that record the elapsed execution time and the stack space usage.
    284282Figure~\ref{itest1} demonstrates one of the outputs of the CerCo C compiler---an embellished version of the original C source code, with cost annotations automatically inserted, the other output being an object code file, not included here.
Note: See TracChangeset for help on using the changeset viewer.