Changeset 3444
- Timestamp:
- Feb 17, 2014, 12:37:33 PM (7 years ago)
- Location:
- Papers/fopara2013
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/fopara2013/fopara13.bib
r3443 r3444 292 292 key = {cerco} 293 293 } 294 295 @misc 296 { jessie, 297 url = {http://krakatoa.lri.fr/}, 298 title = {Jessie {Frama-C} plugin}, 299 key = {jessie} 300 } -
Papers/fopara2013/fopara13.tex
r3443 r3444 931 931 932 932 Not all the details of the non-functional state needs to be exposed, and the 933 technique works better when the part of state that is required can be summari zed933 technique works better when the part of state that is required can be summarised 934 934 in a simple data structure. For example, to handle simple but realistic 935 935 pipelines it is sufficient to remember a short integer that encodes the position … … 957 957 same technique works for loop unrolling without modification: the function will 958 958 assign one cost to the even iterations and another cost to the odd 959 ones. The loopoptimisation code960 that duplicate the loop bodies must also modify the code to correctly propagate959 ones. The optimisation code 960 that duplicates the loop bodies must also modify the code to correctly propagate 961 961 the update of the iteration numbers. The technical details are more complicated and 962 962 can be found in the CerCo reports and publications. The implementation, however, … … 993 993 Frama-C \cite{framac} is a set of analysers for C programs with a 994 994 specification language called ACSL. New analyses can be dynamically added 995 via a plugin system. For instance, the Jessie plugin allows deductive995 via a plugin system. For instance, the Jessie plugin~\cite{jessie} allows deductive 996 996 verification of C programs with respect to their specification in ACSL, with 997 997 various provers as back-end tools. … … 1024 1024 analysis of the VCs associated with branching may lead to a complexity blow up. 1025 1025 1026 \paragraph{Experience with Lustre.} Lustre is a data-flow language for programming1026 \paragraph{Experience with Lustre.} Lustre~\cite{lustre} is a data-flow language for programming 1027 1027 synchronous systems, with a compiler which targets C. We designed a 1028 1028 wrapper for supporting Lustre files. … … 1060 1060 loop in the logic assertions. This logic function takes the variant as a first 1061 1061 parameter. The other parameters of $f$ are the free variables of the body of the 1062 loop. An axiom is added to account the fact that the cost is accumulated at each1062 loop. An axiom is added to account for the fact that the cost is accumulated at each 1063 1063 step of the loop. 1064 1064 The cost of the function is directly added as post-condition of the function. … … 1094 1094 \section{Conclusions and future work} 1095 1095 1096 All the CerCo software and deliverables can be found on the CerCo homepage at~\url{http://cerco.cs.unibo.it}.1096 All CerCo software and deliverables may be found on the project homepage~\cite{cerco}. 1097 1097 1098 1098 The results obtained so far are encouraging and provide evidence that … … 1108 1108 architecture that admits a cost model that is execution history independent. 1109 1109 The most important future work is dealing with hardware architectures 1110 characteri zed by historydependent stateful components, like caches and1110 characterised by history-dependent stateful components, like caches and 1111 1111 pipelines. The main issue is to assign a parametric, dependent cost 1112 1112 to basic blocks that can be later transferred by the labelling approach to
Note: See TracChangeset
for help on using the changeset viewer.