Changeset 3424 for Papers/fopara2013/fopara13.tex
- Timestamp:
- Feb 11, 2014, 12:35:22 PM (7 years ago)
- File:
-
- 1 edited
-
Papers/fopara2013/fopara13.tex (modified) (13 diffs)
Legend:
- Unmodified
- Added
- Removed
-
Papers/fopara2013/fopara13.tex
r3422 r3424 710 710 The hardware state comprises both the functional state that affects the 711 711 computation (the value of the registers and memory) and the non-functional 712 state that does not (the pipeline and cache contents for example). The former is712 state that does not (the pipeline and cache contents, for example). The former is 713 713 in correspondence with the source code state, but reconstructing the 714 714 correspondence may be hard and lifting the cost model to work on the source code 715 715 state is likely to produce cost expressions that are too complex to understand and reason about. 716 Luckily enough, in all modern architectures the cost of executing single716 Fortunately, in all modern architectures the cost of executing single 717 717 instructions is either independent of the functional state or the jitter---the 718 718 difference between the worst and best case execution times---is small enough 719 to be bounded without losing too much precision. Therefore we can concentrate720 on dependencies over the `non-functional' parts of the state only.719 to be bounded without losing too much precision. Therefore we only consider 720 dependencies on the `non-functional' parts of the state. 721 721 722 722 The non-functional state has no correspondence in the high level state and does … … 730 730 update function which is computed during static analysis too. The update 731 731 function associates to each label a function from the recently emitted labels 732 and old state to the new state. It is computed composing the semantics of every732 and old state to the new state. It is computed by composing the semantics of every 733 733 instruction in a basic block and restricting it to the non-functional part of 734 734 the state. … … 745 745 trade precision of the analysis for simplicity by approximating the parametric 746 746 cost with safe non parametric bounds. Interestingly, the functional analysis of 747 the code c andetermine which blocks are executed more frequently in order to748 approximate more aggressively the ones that are executed less.747 the code could determine which blocks are executed more frequently in order to 748 use more aggressive approximations for the ones that are executed least. 749 749 750 750 Dependent labeling can also be applied to allow the compiler to duplicate … … 752 752 a different cost to the different occurrences of a duplicated label. For 753 753 example, loop peeling turns a loop into the concatenation of a copy of the loop 754 body (that executes the first iteration) withthe conditional execution of the755 loop (for the successive iterations). Because of further optimisations,the two756 copies of the loop will be compileddifferently, with the first body usually754 body for the first iteration and the conditional execution of the 755 loop for successive iterations. Further optimisations will compile the two 756 copies of the loop differently, with the first body usually 757 757 taking more time. 758 758 … … 763 763 actual work to be done consists of introducing within the source code, and for each 764 764 loop, a variable that counts the number of iterations. The loop optimisation code 765 that duplicate the loop bodies must also modify the code to propagate correctly765 that duplicate the loop bodies must also modify the code to correctly propagate 766 766 the update of the iteration numbers. The technical details are more complex and 767 767 can be found in the CerCo reports and publications. The implementation, however, … … 834 834 bound on the reaction time of the system. We tested the Cost plugin and the 835 835 Lustre wrapper on the C programs generated by the Lustre compiler. For programs 836 consisting of a few hundred lines of code, the cost plugin computes a WCET and Alt-837 Ergo is able to discharge all VCs automatically.836 consisting of a few hundred lines of code, the cost plugin computes a 837 WCET and Alt-Ergo is able to discharge all VCs automatically. 838 838 839 839 \paragraph{Handling C programs with simple loops.} 840 840 The cost annotations added by the CerCo compiler take the form of C instructions 841 that update by a constant a fresh global variable called the cost variable.842 Synthesizing a WCET of a C function thus consists instatically resolving an841 that update a fresh global variable called the cost variable by a constant. 842 Synthesizing a WCET of a C function thus consists of statically resolving an 843 843 upper bound of the difference between the value of the cost variable before and 844 after the execution of the function, i.e. find in the functionthe instructions844 after the execution of the function, i.e. finding the instructions 845 845 that update the cost variable and establish the number of times they are passed 846 through during the flow of execution. In order to dothe analysis the plugin846 through during the flow of execution. To perform the analysis the plugin 847 847 makes the following assumptions on the programs: 848 848 1) there are no recursive functions; … … 886 886 887 887 \subsection{The CerCo compiler} 888 In CerCo we have developed a certain number ofcost preserving compilers based888 In CerCo we have developed several cost preserving compilers based 889 889 on the labeling approach. Excluding an initial certified compiler for a `while' 890 890 language, all remaining compilers target realistic source languages---a pure … … 901 901 advanced optimisations yet. Its user interface, however, is the same as the one 902 902 of the other versions, in order to trade safety with additional performances. In 903 particular, the Frama-C CerCo plugin can work without recompilation with all904 compilers.903 particular, the Frama-C CerCo plugin can work without recompilation 904 with all of our C compilers. 905 905 906 906 The 8051/8052 microprocessor is a very simple one, with constant-cost … … 919 919 The CerCo compiler is loosely based on the CompCert compiler \cite{compcert}, a 920 920 recently developed certified compiler from C to the PowerPC, ARM and x86 921 microprocessors. Contraryto CompCert, both the CerCo code and its922 certification are open source. Some data structures and language definitions for921 microprocessors. In contrast to CompCert, both the CerCo code and its 922 certification are fully open source. Some data structures and language definitions for 923 923 the front-end are directly taken from CompCert, while the back-end is a redesign 924 924 of a compiler from Pascal to MIPS used by Fran\c{c}ois Pottier for a course at the 925 925 Ecole Polytechnique. 926 926 927 The main peculiarities of the CerCo compiler are the following.927 The main differences in the CerCo compiler are: 928 928 \begin{enumerate} 929 929 \item All the intermediate languages include label emitting instructions to … … 933 933 the way down to object code in order to perform the static analysis. Therefore 934 934 we integrated also an optimising assembler and a static analyser. 935 \item In order to avoid implementing a linker and a loader, we do not support separate 936 compilation and external calls. Adding them is a transparent 937 process to the labeling approach and should create no unknown problem. 938 \item We target an 8-bit processor, in contrast to CompCert's 32-bit targets. Targeting an 8-bit processor requires 939 several changes and increased code size, but it is not fundamentally more 935 \item In order to avoid the additional work of implementing a linker 936 and a loader, we do not support separate 937 compilation and external calls. Adding them is orthogonal 938 to the labeling approach and should not introduce extra problems. 939 \item We target an 8-bit processor, in contrast to CompCert's 32-bit targets. This requires 940 many changes and more compiler code, but it is not fundamentally more 940 941 complex. The proof of correctness, however, becomes much harder. 941 942 \item We target a microprocessor that has a non uniform memory model, which is … … 953 954 We implemented the 954 955 CerCo compiler in the interactive theorem prover Matita and have formally 955 certified that the cost model induced on the source code correctly and precisely956 predicts the object code behaviour. We actually induce two cost models, one for956 certified that the cost models induced on the source code correctly and precisely 957 predicts the object code behaviour. There are two cost models, one for execution 957 958 time and one for stack space consumption. We show the correctness of the prediction 958 959 only for those programs that do not exhaust the available machine stack space, a … … 964 965 proof for non-functional properties, we have introduced a new semantics for 965 966 programming languages based on a new kind of structured observables with the 966 relative notions of forward similarity and the study of the inten tional967 relative notions of forward similarity and the study of the intensional 967 968 consequences of forward similarity. We have also introduced a unified 968 969 representation for back-end intermediate languages that was exploited to provide … … 1021 1022 I/O operations can be performed in the prefix of the run, but not in the 1022 1023 measurable sub-run. Therefore we prove that we can predict reaction times, but 1023 not I/O times, as it should be.1024 not I/O times, as desired. 1024 1025 1025 1026 \section{Conclusions and future work}
Note: See TracChangeset
for help on using the changeset viewer.
