Changeset 3435
- Timestamp:
- Feb 14, 2014, 5:37:31 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/fopara2013/fopara13.tex
r3434 r3435 887 887 connection is established, any cost model computed on the object code can be 888 888 transferred to the source code, without affecting the code of the compiler or 889 its proof. In particular, it is immediate that we can also transport cost models 890 that associate to each label functions from hardware state to natural numbers. 891 However, a problem arises during the instrumentation phase that replaces cost 892 emission statements with increments of global cost variables. The global cost 893 variable must be incremented with the result of applying the function associated 894 to the label to the hardware state at the time of execution of the block. 895 The hardware state comprises both the functional state that affects the 889 its proof. In particular, we can also transport cost models 890 that associate to each label a \emph{function} from the hardware state 891 to a natural number. 892 However, a problem arises during the instrumentation phase that replaces label 893 emission statements with increments of global cost variables. They are 894 incremented by the result of applying the label's cost function 895 to the hardware state at the time of execution of the block. However, 896 the hardware state comprises both the functional state that affects the 896 897 computation (the value of the registers and memory) and the non-functional 897 state that does not (the pipeline and cache contents, for example). The former is898 in correspondence with the source code state, but reconstructing the898 state that does not (the pipeline and cache contents, for example). 899 We can find corresponding information for the former in the source code state, but constructing the 899 900 correspondence may be hard and lifting the cost model to work on the source code 900 901 state is likely to produce cost expressions that are too complex to understand and reason about. 901 Fortunately, in allmodern architectures the cost of executing single902 Fortunately, in modern architectures the cost of executing single 902 903 instructions is either independent of the functional state or the jitter---the 903 904 difference between the worst and best case execution times---is small enough … … 914 915 state and another one that remembers the last few labels emitted. The 915 916 state variable must be updated at every label emission statement, 916 using an update function which is computed during static analysis 917 too. The update function associates to each label a function from the 917 using an update function which is computed during the processor timing 918 analysis. 919 This update function assigns to each label a function from the 918 920 recently emitted labels and old state to the new state. It is computed 919 by composing the semantics of every instruction in a basic block and920 restrict ing itto the non-functional part of the state.921 by composing the semantics of every instruction in a basic block 922 restricted to the non-functional part of the state. 921 923 922 924 Not all the details of the non-functional state needs to be exposed, and the … … 927 929 for the user to understand the meaning of the state to reason over the properties 928 930 of the 929 program. Moreover, at any momentthe user, or the invariant generator tools that931 program. Moreover, the user, or the invariant generator tools that 930 932 analyse the instrumented source code produced by the compiler, can decide to 931 933 trade precision of the analysis for simplicity by approximating the 932 cost withsafe bounds that do not depend on the processor state. Interestingly, the functional analysis of934 cost by safe bounds that do not depend on the processor state. Interestingly, the functional analysis of 933 935 the code could determine which blocks are executed more frequently in order to 934 use more aggressive approximations for th e onesthat are executed least.936 use more aggressive approximations for those that are executed least. 935 937 936 938 Dependent labelling can also be applied to allow the compiler to duplicate … … 945 947 By introducing a variable that keeps track of the iteration number, we can 946 948 associate to the label a cost that is a function of the iteration number. The 947 same technique works for loop unrolling without modifications: the function will 948 assign a cost to the even iterations and another cost to the odd ones. The 949 actual work to be done consists of introducing within the source code, and for each 950 loop, a variable that counts the number of iterations. The loop optimisation code 949 same technique works for loop unrolling without modification: the function will 950 assign one cost to the even iterations and another cost to the odd 951 ones. The loop optimisation code 951 952 that duplicate the loop bodies must also modify the code to correctly propagate 952 the update of the iteration numbers. The technical details are more compl exand953 the update of the iteration numbers. The technical details are more complicated and 953 954 can be found in the CerCo reports and publications. The implementation, however, 954 955 is quite simple (and forms part of our OCaml version of the compiler)
Note: See TracChangeset
for help on using the changeset viewer.