Changeset 1688


Ignore:
Timestamp:
Feb 13, 2012, 9:08:40 AM (6 years ago)
Author:
amadio
Message:

up d5.1-5.3

Location:
Deliverables/D5.1-5.3
Files:
3 added
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D5.1-5.3/report.tex

    r1659 r1688  
    514514\newcommand{\compcert}{{\sf CompCert}}
    515515%\newcommand{\cerco}{{\sf CerCo}}
     516\newcommand{\cost}{{\sf Cost}}
     517\newcommand{\lamcost}{\sf LamCost}
    516518\newcommand{\cil}{{\sf CIL}}
    517519\newcommand{\scade}{{\sf Scade}}
     
    572574\begin{large}
    573575Main Authors:\\
    574 Roberto M.~Amadio, Nicolas~Ayache, Yann~R\'egis-Gianas,
     576Roberto M.~Amadio, Nicolas~Ayache, Yann~R\'egis-Gianas, Paolo Tranquilli
    575577\end{large}
    576578\end{center}
     
    590592
    591593\paragraph{Summary}
     594The deliverable D5.1-D5.3 is composed of the following parts:
     595
     596\begin{enumerate}
     597
     598\item This summary.
     599
     600\item The paper \cite{A12} and the related software $\cost$.
     601
     602\item The paper \cite{T12} and the related software.
     603
     604\item The paper \cite{ARG11} and the related software $\lamcost$.
     605
     606\item The paper \cite{MA11}.
     607
     608\end{enumerate}
     609
     610This document and the softwares above can be downloaded at the
     611page:
     612\begin{center}
     613{\tt http://cerco.cs.unibo.it/}
     614\end{center}
     615
     616{\scriptsize
     617\begin{thebibliography}{99}
     618
     619
     620\bibitem{A12}
     621N.~Ayache.
     622\newblock Synthesis of certified cost bounds.
     623\newblock Universit\'e Paris Diderot. Internal report documenting the $\cost$ software, 2012.
     624
     625
     626\bibitem{ARG11}
     627R.M.~Amadio, Y.~R\'egis-Gianas.
     628\newblock Certifying and reasoning on cost annotations of functional programs.
     629\newblock In Proc. FOPARA, Springer LNCS (to appear), 2012.
     630\newblock Also Research Report, Universit\'e Paris Diderot,
     631{\tt http://hal.inria.fr/inria-00629473/en/}, 2011.
     632
     633
     634\bibitem{MA11}
     635A.~Madet, R.M.~Amadio.
     636\newblock An Elementary Affine $\lambda$-Calculus with Multithreading and Side Effects.
     637\newblock In Proc. TLCA, Springer LNCS 6690:138-152, 2011.
     638\newblock Also Research Report, Universit\'e Paris Diderot,
     639{\tt http://hal.archives-ouvertes.fr/hal-00569095/fr/}, 2011.
     640
     641\bibitem{T12}
     642P.~Tranquilli.
     643\newblock Indexed labels for loop iteration dependent costs.
     644\newblock Universit\`a di Bologna. Internal report documenting the indexed labels software, 2012.
     645
     646\end{thebibliography}}
     647
     648\newpage
     649
     650\paragraph{Aim}
    592651The main aim of WP5 is to develop proof of concept prototypes where
    593 the (untrusted) compiler developed in WP2 is interfaced with existing tools
     652the (untrusted) compiler implemented in WP2 is interfaced with existing tools
    594653in order to synthesize complexity  assertions on the execution
    595654time of programs. Eventually, the approach should be adapted to
     
    597656month 36).
    598657
    599 In particular, the main planned contribution of deliverable D5.1 is a
    600 tool that takes as input an annotated C program produced by the CerCo
    601 compiler and tries to synthesize a certified bound on the execution
    602 time of the program.  The related expected contribution of deliverable
    603 D5.3 amounts to apply the developed tool to the C programs generated
    604 by a Lustre compiler.  This planned work is described in the first
    605 document...which accompanies a software distribution...
    606 Frama-C plug-in ...more examples...
    607 
    608 We pause to recall a redistribution of the workforce of the UDP site.
     658
     659\paragraph{Synthesis of certified cost bounds}
     660The main planned contribution of deliverable D5.1 is a tool that takes
     661as input an annotated $\C$ program produced by the $\cerco$ compiler
     662and tries to synthesize a certified bound on the execution time of the
     663program.  The related expected contribution of deliverable D5.3
     664amounts to apply the developed tool to the $\C$ programs generated by
     665a $\lustre$ compiler.  This work is described in the first document
     666\cite{A12} which accompanies a software distribution called $\cost$.
     667The development takes the form of a `$\framac$ plug-in'.  $\framac$ is
     668an open source and well-established platform to reason formally on
     669$\C$ programs. The proof obligations generated from Hoare style
     670assertions on $\C$ programs are passed to a small number of provers
     671that try to discharge them automatically. The platform has been
     672designed to be extensible by means of so called plug-in's written in
     673$\ocaml$.  The $\cost$ software is a $\framac$ plug-in which in first
     674approximation takes the following actions: (1) it receives as input a
     675$\C$ program, (2) it applies the $\cerco$ compiler to produce a
     676related $\C$ program with cost annotations, (3) it applies some
     677heuristics to produce a tentative bound on the cost of executing a
     678$\C$ function as a function of the value of its parameters, (4) it
     679calls the provers embedded in the $\framac$ tool to discharge the
     680related proof obligations.  The current size of the $\cost$ plug-in is
     6814K lines of $\ocaml$ code.  More details are available in the first
     682part of the document \cite{A12}.  The second part of the document
     683(formally, corresponding to deliverable D5.3) tries to delimit the
     684practical applicability of the plug-in. To this end, the tool has been
     685applied to the $\C$ code generated by the $\lustre$ compiler and to
     686some other simple $\C$ programs.
     687
     688We pause to recall a redistribution of the workforce of the UPD site.
    609689Following the resignation of the doctoral student at the end of year
    610 1, the contract of the post-doc has been as extended till month ??  It
    611 follows that in the UPD site there has been a shift of manpower from
    612 the third to the second year. Because of this shift we decided to
     6901, the contract of the post-doc has been extended till month 33.
     691It follows that in the UPD site there has been a shift of manpower
     692from the third to the second year. Because of this shift we decided to
    613693anticipate the presentation of deliverable D5.3 at month 24 rather
    614 than month 36.
    615 
     694than month 36. Besides this contingent reason, it is clear that the
     695development of the synthesis tool must go hand in hand with its
     696experimentation on larger and larger classes of programs.  The UPD
     697post-doc is expected to continue work on D5.1 and D5.3 till the end of
     698its contract.
     699
     700
     701\paragraph{Indexed labels for loop iteration dependent costs}
     702The first year scientific review report, among other things, contrasts
     703the $\cerco$ approach with the one adopted in tools such as $\absint$
     704which are used by the WCET community and it recommends that the
     705approach to cost annotations described in WP2 is made {\em coarser},
     706{\em i.e.}, that a label covers a larger portion of code.  During the
     707second year, most of the work of a post-doc at UNIBO was aimed at
     708addressing this remark \cite{T12}.  This has resulted in a refinement
     709of the labelling approach into a so called {\em indexed labelling}.
     710It consists in formally indexing cost labels with the iterations of
     711the containing loops they occur in within the source code.  These
     712indexes can be transformed during the compilation, and when lifted
     713back to source code they produce dependent costs. Preliminary
     714experiments suggest that this refinement allows to retain preciseness
     715when the program is subject to loop transformations such as loop
     716peeling and loop unrolling.  A prototype implementation has been
     717developed on top of the untrusted $\cerco$ compiler D2.2.
     718
     719
     720% so as to take into account the effects of
     721%% cache memories and pipelines. Following this suggestion
     722%% a post-doc at UB has worked on these issues and we have invited
     723%% C. Ferdinand to present the AbsInt tool.
     724%% (*** Lack of compositionality --- timing anomalies --- ***)
     725
     726
     727
     728\paragraph{Certifying and reasoning on cost annotations of functional programs}
    616729During the second year some unplanned work related to deliverables
    617 D5.1 and D5.3 has taken place at UPD.
    618 
    619 The main development concerns the extension of the CerCo labelling
    620 approach to a standard compilation chain from a higher-order
    621 functional language of the ML family to C and the development of
    622 framework to reason about the cost annotations. This work shows...the
    623 generality of the approach...  Parallel the work done for C...
    624 Ongoing work tries to produce valid garbage collection statements by
    625 typing...
    626 
    627 A second development is of a more speculative nature and
    628 concerned with the development of a type system
    629 for a functional langauge with side effects that guarantees a complexity
    630 bound... First work to account for side effects... Ongoing work tries to
    631 extend the framework to polynomial time. Eventually we hope to join
    632 the thread on implicit complexity???
     730D5.1 and D5.3 has taken place at UPD.  The main development
     731\cite{ARG11} concerns the extension of the $\cerco$ labelling approach
     732described in D2.1 to a standard compilation chain from a higher-order
     733functional language of the $\ml$ family to $\C$.  This
     734work shows that the approach is sufficiently general to be applied to
     735higher-order programs whose concrete complexity is generally regarded
     736as difficult to estimate.  Moreover, the introduction of
     737higher-order functions calls for a higher-order logic to reason on the
     738cost annotations.  In this respect, we have built on previous work by
     739one of the authors on a higher-order Hoare logic. Starting from a
     740(higher-order) specification of the expected cost of a function our
     741tool $\lamcost$ produces automatically a list of proof obligations. Preliminary
     742experiments suggest that a large part of these proof obligations can
     743be discharged automatically and that the remaining ones can be proved
     744in a proof assistant such as $\coq$.  Ongoing work that should be
     745completed within the third year of the project is extending the
     746compilation chain and the cost analysis to include garbage collection
     747using a {\em region based} memory management \`a la Tofte-Talpin.
     748
     749\paragraph{An Elementary Affine $\lambda$-Calculus with Multithreading and Side Effects.}
     750A second development at UPD is of a more speculative nature and is
     751concerned with the design of a type system for a functional language
     752with side effects that guarantees complexity bounds. As far as we
     753know, this is the first work that accounts for side effects. The
     754obtained result concerns {\em elementary time} and ongoing work that
     755should be completed within the third year of the project concerns a
     756similar result for {\em polynomial time}.  We regard this work as a
     757step towards bridging the $\cerco$ approach with the work on {\em
     758  Implicit computational complexity} (ICC) in which our universities
     759are also involved (in 2011, the $\cerco$ project organised in Paris a
     760joint workshop with an ICC oriented project).  As a matter of fact,
     761there is still a large gap to be filled before the results in ICC can
     762have an impact on the practice of programming.
     763
     764
    633765
    634766
     
    641773\newpage
    642774
     775\includepdf[pages={-}]{tranquilli.pdf}
     776
     777\newpage
     778
     779
    643780\includepdf[pages={-}]{fopara.pdf}
    644781
Note: See TracChangeset for help on using the changeset viewer.