Changeset 3339 for Papers/fopara2013/fopara13.tex
- Timestamp:
- Jun 7, 2013, 6:02:21 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/fopara2013/fopara13.tex
r3337 r3339 110 110 \section{Introduction} 111 111 112 \paragraph{Problem statement } Computer programs can be specified with both112 \paragraph{Problem statement.} Computer programs can be specified with both 113 113 functional constraints (what a program must do) and non-functional constraints 114 114 (e.g. what resources---time, space, etc.---the program may use). In the current … … 130 130 the estimates. 131 131 132 \paragraph{Vision and approach } We want to reconcile functional and132 \paragraph{Vision and approach.} We want to reconcile functional and 133 133 non-functional analyses: to share information and perform both at the same time 134 134 on source code. … … 155 155 components. 156 156 157 \paragraph{Contributions } We have developed what we refer to as \emph{the labeling approach} \cite{labeling}, a157 \paragraph{Contributions.} We have developed what we refer to as \emph{the labeling approach} \cite{labeling}, a 158 158 technique to implement compilers that induce cost models on source programs by 159 159 very lightweight tracking of code changes through compilation. We have studied … … 449 449 \begin{lstlisting} 450 450 |int __cost = 33; int __stack = 5, __stack_max = 5;| 451 452 451 |void __cost_incr(int incr) { __cost = __cost + incr; }| 453 454 452 |void __stack_incr(int incr) { 455 453 __stack = __stack + incr; … … 478 476 /*@ for time_cost: loop invariant 479 477 __cost <= 480 \at(__cost,__l)+220*(__max(\at(5-j,__l), 0)-__max (5-j, 0)); 478 \at(__cost,__l)+220*(__max(\at(5-j,__l), 0) 479 -__max (5-j, 0)); 481 480 for stack_cost: loop invariant 482 481 __stack_max == \at(__stack_max,__l); … … 509 508 \label{itest1} 510 509 \end{figure} 511 \section{Main S\&T results of the CerCo project}512 We will now review the main S\&T results achieved in the CerCo project.510 \section{Main scientific and technical results} 511 We will now review the main results that the CerCo project has achieved. 513 512 514 513 % \emph{Dependent labeling~\cite{?}.} The basic labeling approach assumes a … … 569 568 bounded by a program-dependent constant (precision property). 570 569 571 \paragraph{The labeling software components } We solve the problem in four570 \paragraph{The labeling software components.} We solve the problem in four 572 571 stages \cite{labeling}, implemented by four software components that are used 573 572 in sequence. … … 615 614 The obtained source code is the instrumented source code. 616 615 617 \paragraph{Correctness } Requirements 1, 2 and 3 of the problem statement616 \paragraph{Correctness.} Requirements 1, 2 and 3 of the problem statement 618 617 obviously hold, with 2 and 3 being a consequence of the definition of a correct 619 618 labeling preserving compiler. It is also obvious that the value of the global … … 765 764 a proof automatically, otherwise, user interaction is required. 766 765 767 \paragraph{The Cost plugin and its application to the Lustre compiler }766 \paragraph{The Cost plugin and its application to the Lustre compiler.} 768 767 Frama-C \cite{framac} is a set of analysers for C programs with a 769 768 specification language called ACSL. New analyses can be dynamically added … … 784 783 Lustre compiler. 785 784 786 \paragraph{Soundness } The soundness of the whole framework depends on the cost785 \paragraph{Soundness.} The soundness of the whole framework depends on the cost 787 786 annotations added by the CerCo compiler, the synthetic costs produced by the 788 787 cost plugin, the verification conditions (VCs) generated by Jessie, and the … … 799 798 composed of branching and assignments (no loops and no recursion) because a fine 800 799 analysis of the VCs associated with branching may lead to a complexity blow up. 801 \paragraph{Experience with Lustre } Lustre is a data-flow language for programming800 \paragraph{Experience with Lustre.} Lustre is a data-flow language for programming 802 801 synchronous systems, with the language coming with a compiler to C. We designed a 803 802 wrapper for supporting Lustre files. … … 809 808 Ergo is able to discharge all VCs automatically. 810 809 811 \paragraph{Handling C programs with simple loops }810 \paragraph{Handling C programs with simple loops.} 812 811 The cost annotations added by the CerCo compiler take the form of C instructions 813 812 that update by a constant a fresh global variable called the cost variable. … … 844 843 2) by annotating functions with cost specifications. The plugin will use this cost 845 844 for the function instead of computing it. 846 \paragraph{C programs with pointers }845 \paragraph{C programs with pointers.} 847 846 When it comes to verifying programs involving pointer-based data structures, 848 847 such as linked lists, trees, or graphs, the use of traditional first-order logic … … 897 896 Ecole Polytechnique. 898 897 899 The main peculiarities of the CerCo compiler are :898 The main peculiarities of the CerCo compiler are the following. 900 899 \begin{enumerate} 901 \item all of ourintermediate languages include label emitting instructions to902 implement the labeling approach, and the compiler preserves execution traces ,903 \item traditionally compilers target an assembly language with additional900 \item All the intermediate languages include label emitting instructions to 901 implement the labeling approach, and the compiler preserves execution traces. 902 \item Traditionally compilers target an assembly language with additional 904 903 macro-instructions to be expanded before assembly; for CerCo we need to go all 905 904 the way down to object code in order to perform the static analysis. Therefore 906 we integrated also an optimising assembler and a static analyser ,907 \item to avoid implementing a linker and a loader, we do not support separate908 compilation and external calls. Adding a linker and a loaderis a transparent909 process to the labeling approach and should create no unknown problem ,910 \item we target an 8-bit processor. Targeting an 8-bit processor requires905 we integrated also an optimising assembler and a static analyser. 906 \item In order to avoid implementing a linker and a loader, we do not support separate 907 compilation and external calls. Adding them is a transparent 908 process to the labeling approach and should create no unknown problem. 909 \item We target an 8-bit processor. Targeting an 8-bit processor requires 911 910 several changes and increased code size, but it is not fundamentally more 912 complex. The proof of correctness, however, becomes much harder ,913 \item we target a microprocessor that has a non uniform memory model, which is911 complex. The proof of correctness, however, becomes much harder. 912 \item We target a microprocessor that has a non uniform memory model, which is 914 913 still often the case for microprocessors used in embedded systems and that is 915 914 becoming common again in multi-core processors. Therefore the compiler has to 916 915 keep track of data and it must move data between memory regions in the proper 917 way. Alsothe size of pointers to different regions is not uniform. An916 way. Moreover the size of pointers to different regions is not uniform. An 918 917 additional difficulty was that the space available for the stack in internal 919 918 memory in the 8051 is tiny, allowing only a minor number of nested calls. To … … 947 946 out to be more complex than what we expected at the beginning. 948 947 949 \paragraph{The statement }948 \paragraph{The statement.} 950 949 Real time programs are often reactive programs that loop forever responding to 951 950 events (inputs) by performing some computation followed by some action (output) … … 1028 1027 to evaluate the CerCo's prototype on realistic, industrial-scale programs. 1029 1028 1030 \bibliographystyle{llncs} 1031 \begin{thebibliography}{19} 1032 1033 \bibitem{survey} \textbf{A Survey of Static Program Analysis Techniques} 1034 W.~W\"ogerer. Technical report. Technische Universit\"at Wien 2005 1035 1036 \bibitem{cerco} \textbf{Certified Complexity}. R.M. Amadio, A. Asperti, N. Ayache, 1037 B. Campbell, D. P. Mulligan, R. Pollack, Y. Regis-Gianas, C. Sacerdoti Coen, I. 1038 Stark, in Procedia Computer Science, Volume 7, 2011, Proceedings of the 2 nd 1039 European Future Technologies Conference and Exhibition 2011 (FET 11), 175-177. 1040 1041 \bibitem{labeling} \textbf{Certifying and Reasoning on Cost Annotations in C 1042 Programs}, N. Ayache, R.M. Amadio, Y.R\'{e}gis-Gianas, in Proc. FMICS, Springer 1043 LNCS 1044 7437: 32-46, 2012. 1045 %, DOI:10.1007/978-3-642-32469-7\_3. 1046 1047 \bibitem{labeling2} \textbf{Certifying and reasoning on cost annotations of 1048 functional programs}. 1049 R.M. Amadio, Y. R\'{e}gis-Gianas. Proceedings of the Second international conference 1050 on Foundational and Practical Aspects of Resource Analysis FOPARA 2011 Springer 1051 LNCS 7177:72-89, 2012. 1052 1053 \bibitem{compcert} \textbf{Formal verification of a realistic compiler}. X. Leroy, In Commun. ACM 52(7), 107–115, 2009. 1054 1055 \bibitem{framac} \textbf{Frama-C user manual}. L. Correnson, P. Cuoq, F. Kirchner, V. Prevosto, A. Puccetti, J. Signoles, 1056 B. Yakobowski. in CEA-LIST, Software Safety Laboratory, Saclay, F-91191, 1057 \url{http://frama-c.com/}. 1058 1059 \bibitem{paolo} \textbf{Indexed Labels for Loop Iteration Dependent Costs}. P. 1060 Tranquilli, in Proceedings of the 11th International Workshop on Quantitative 1061 Aspects of Programming Languages and Systems (QAPL 2013), Rome, 23rd-24th March 1062 2013, Electronic Proceedings in Theoretical Computer Science, to appear in 2013. 1063 1064 \bibitem{separation} \textbf{Intuitionistic reasoning about shared mutable data 1065 structure} J.C. Reynolds. In Millennial Perspectives in Computer Science, 1066 pages 303–321, Houndsmill, Hampshire, 2000. Palgrave. 1067 1068 \bibitem{lustre} \textbf{LUSTRE: a declarative language for real-time 1069 programming} 1070 P. Caspi, D. Pilaud, N. Halbwachs, J.A. Plaice. In Proceedings of 1071 the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages ACM 1072 1987. 1073 1074 \bibitem{correctness} \textbf{On the correctness of an optimising assembler for 1075 the intel MCS-51 microprocessor}. 1076 D. P. Mulligan, C. Sacerdoti Coen. In Proceedings of the Second 1077 international conference on Certified Programs and Proofs, Springer-Verlag 2012. 1078 1079 \bibitem{proartis} \textbf{PROARTIS: Probabilistically Analysable Real-Time 1080 Systems}, F.J. Cazorla, E. Qui\~{n}ones, T. Vardanega, L. Cucu, B. Triquet, G. 1081 Bernat, E. Berger, J. Abella, F. Wartel, M. Houston, et al., in ACM Transactions 1082 on Embedded Computing Systems, 2012. 1083 1084 \bibitem{embounded} \textbf{The EmBounded project (project paper)}. K. Hammond, 1085 R. Dyckhoff, C. Ferdinand, R. Heckmann, M. Hofmann, H. Loidl, G. Michaelson, J. 1086 Serot, A. Wallace, in Trends in Functional Programming, Volume 6, Intellect 1087 Press, 2006. 1088 1089 \bibitem{matita} 1090 \textbf{The Matita Interactive Theorem Prover}. 1091 A. Asperti, C. Sacerdoti Coen, W. Ricciotti, E. Tassi. 1092 23rd International Conference on Automated Deduction, CADE 2011. 1093 1094 \bibitem{typeffects} \textbf{The Type and Effect Discipline}. J.-P. Talpin, 1095 P. Jouvelot. 1096 In Proceedings of the Seventh Annual Symposium on Logic in Computer Science 1097 (LICS '92), Santa Cruz, California, USA, June 22-25, 1992. 1098 IEEE Computer Society 1992. 1099 1100 \bibitem{stateart} \textbf{The worst-case execution-time problem overview of 1101 methods 1102 and survey of tools.} R. Wilhelm et al., in ACM Transactions on Embedded 1103 Computing Systems, 7:1–53, May 2008. 1104 1105 %\bibitem{proartis2} \textbf{A Cache Design for Probabilistic Real-Time 1106 % Systems}, L. Kosmidis, J. Abella, E. Quinones, and F. Cazorla, in Design, 1107 % Automation, and Test in Europe (DATE), Grenoble, France, 03/2013. 1108 1109 \end{thebibliography} 1029 % \bibliographystyle{splncs} 1030 \bibliography{fopara13} 1031 % \begin{thebibliography}{19} 1032 % 1033 % \bibitem{survey} \textbf{A Survey of Static Program Analysis Techniques} 1034 % W.~W\"ogerer. Technical report. Technische Universit\"at Wien 2005 1035 % 1036 % \bibitem{cerco} \textbf{Certified Complexity}. R.M. Amadio, A. Asperti, N. Ayache, 1037 % B. Campbell, D. P. Mulligan, R. Pollack, Y. Regis-Gianas, C. Sacerdoti Coen, I. 1038 % Stark, in Procedia Computer Science, Volume 7, 2011, Proceedings of the 2 nd 1039 % European Future Technologies Conference and Exhibition 2011 (FET 11), 175-177. 1040 % 1041 % \bibitem{labeling} \textbf{Certifying and Reasoning on Cost Annotations in C 1042 % Programs}, N. Ayache, R.M. Amadio, Y.R\'{e}gis-Gianas, in Proc. FMICS, Springer 1043 % LNCS 1044 % 7437: 32-46, 2012. 1045 % %, DOI:10.1007/978-3-642-32469-7\_3. 1046 % 1047 % \bibitem{labeling2} \textbf{Certifying and reasoning on cost annotations of 1048 % functional programs}. 1049 % R.M. Amadio, Y. R\'{e}gis-Gianas. Proceedings of the Second international conference 1050 % on Foundational and Practical Aspects of Resource Analysis FOPARA 2011 Springer 1051 % LNCS 7177:72-89, 2012. 1052 % 1053 % \bibitem{compcert} \textbf{Formal verification of a realistic compiler}. X. Leroy, In Commun. ACM 52(7), 107–115, 2009. 1054 % 1055 % \bibitem{framac} \textbf{Frama-C user manual}. L. Correnson, P. Cuoq, F. Kirchner, V. Prevosto, A. Puccetti, J. Signoles, 1056 % B. Yakobowski. in CEA-LIST, Software Safety Laboratory, Saclay, F-91191, 1057 % \url{http://frama-c.com/}. 1058 % 1059 % \bibitem{paolo} \textbf{Indexed Labels for Loop Iteration Dependent Costs}. P. 1060 % Tranquilli, in Proceedings of the 11th International Workshop on Quantitative 1061 % Aspects of Programming Languages and Systems (QAPL 2013), Rome, 23rd-24th March 1062 % 2013, Electronic Proceedings in Theoretical Computer Science, to appear in 2013. 1063 % 1064 % \bibitem{separation} \textbf{Intuitionistic reasoning about shared mutable data 1065 % structure} J.C. Reynolds. In Millennial Perspectives in Computer Science, 1066 % pages 303–321, Houndsmill, Hampshire, 2000. Palgrave. 1067 % 1068 % \bibitem{lustre} \textbf{LUSTRE: a declarative language for real-time 1069 % programming} 1070 % P. Caspi, D. Pilaud, N. Halbwachs, J.A. Plaice. In Proceedings of 1071 % the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages ACM 1072 % 1987. 1073 % 1074 % \bibitem{correctness} \textbf{On the correctness of an optimising assembler for 1075 % the intel MCS-51 microprocessor}. 1076 % D. P. Mulligan, C. Sacerdoti Coen. In Proceedings of the Second 1077 % international conference on Certified Programs and Proofs, Springer-Verlag 2012. 1078 % 1079 % \bibitem{proartis} \textbf{PROARTIS: Probabilistically Analysable Real-Time 1080 % Systems}, F.J. Cazorla, E. Qui\~{n}ones, T. Vardanega, L. Cucu, B. Triquet, G. 1081 % Bernat, E. Berger, J. Abella, F. Wartel, M. Houston, et al., in ACM Transactions 1082 % on Embedded Computing Systems, 2012. 1083 % 1084 % \bibitem{embounded} \textbf{The EmBounded project (project paper)}. K. Hammond, 1085 % R. Dyckhoff, C. Ferdinand, R. Heckmann, M. Hofmann, H. Loidl, G. Michaelson, J. 1086 % Serot, A. Wallace, in Trends in Functional Programming, Volume 6, Intellect 1087 % Press, 2006. 1088 % 1089 % \bibitem{matita} 1090 % \textbf{The Matita Interactive Theorem Prover}. 1091 % A. Asperti, C. Sacerdoti Coen, W. Ricciotti, E. Tassi. 1092 % 23rd International Conference on Automated Deduction, CADE 2011. 1093 % 1094 % \bibitem{typeffects} \textbf{The Type and Effect Discipline}. J.-P. Talpin, 1095 % P. Jouvelot. 1096 % In Proceedings of the Seventh Annual Symposium on Logic in Computer Science 1097 % (LICS '92), Santa Cruz, California, USA, June 22-25, 1992. 1098 % IEEE Computer Society 1992. 1099 % 1100 % \bibitem{stateart} \textbf{The worst-case execution-time problem overview of 1101 % methods 1102 % and survey of tools.} R. Wilhelm et al., in ACM Transactions on Embedded 1103 % Computing Systems, 7:1–53, May 2008. 1104 % 1105 % %\bibitem{proartis2} \textbf{A Cache Design for Probabilistic Real-Time 1106 % % Systems}, L. Kosmidis, J. Abella, E. Quinones, and F. Cazorla, in Design, 1107 % % Automation, and Test in Europe (DATE), Grenoble, France, 03/2013. 1108 % 1109 % \end{thebibliography} 1110 1110 1111 1111
Note: See TracChangeset
for help on using the changeset viewer.