Changeset 666 for Deliverables/D1.1/Presentations
- Timestamp:
- Mar 10, 2011, 1:20:47 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D1.1/Presentations/WP2-roberto.tex
r656 r666 512 512 Implement a {\bf proof-of-concept prototype} of the cost annotating compiler. 513 513 514 {\small 514 515 \begin{description} 515 516 … … 529 530 \item[D2.2] Untrusted cost-annotating $\ocaml$ compiler (T0+12). 530 531 531 \end{description} 532 \end{description}} 533 532 534 {\small \Red{\NB} This first part is an {\bf introduction} to Tasks 2.1 and 2.2. The 533 535 second part will give more details on Task 2.2, discuss Task 2.3 (with demo), … … 535 537 536 538 \end{frame} 539 540 541 537 542 538 543 … … 562 567 563 568 564 565 566 567 568 569 570 571 572 573 574 575 576 \begin{frame} 577 578 \frametitle{Motivation} 579 Resource analysis of programming models should, if we are serious about it, 580 eventually have an impact on programming practice. Limiting factors include: 581 582 \begin{itemize} 583 584 \item Bounds are {\bf asymptotic} and sometimes a bit {\bf shaky} (exotic compilers): we need an effort to make them concrete and reliable. 585 586 \item Should focus on software applications that {\bf do care about resource bounds}. E.g., focus on embedded programs rather than on pure functional programs. 587 588 \item Implicit complexity programming languages are a straight jacket: {\bf restrictions} are often complex and too difficult to program with. 589 590 \end{itemize} 591 592 \end{frame} 593 594 595 \begin{frame} 596 597 \frametitle{$\cerco$ goals and approach} 569 \begin{frame} 570 571 \frametitle{$\cerco$ goals and approach (again)} 598 572 599 573 \begin{itemize} … … 621 595 622 596 623 \begin{frame} 624 625 \frametitle{Current technology and our challenge} 626 \begin{itemize} 627 628 629 \item Compilation phases are heavily {\bf inspected and tested} 630 but not formally checked with a proof assistant. 631 \[ 632 \lustre \arrow \C \arrow \textsc{binary~ code} 633 \] 634 \item Binary code must be {\bf annotated} with (uncertified) 635 information on the number of iterations of loops. 636 637 \item Tools such as \textsc{AbsInt} perform WCET analysis of 638 {\bf sequences of instructions of binary code}. 597 598 \begin{frame} 599 600 \frametitle{More motivation} 601 Resource analysis of programming models should, if we are serious about it, 602 eventually have an impact on programming practice. Limiting factors include: 603 604 \begin{itemize} 605 606 \item Bounds are {\bf asymptotic} and sometimes a bit {\bf shaky} (exotic compilers): we need an effort to make them concrete and reliable. 607 608 \item Should focus on software applications that {\bf do care about resource bounds}. E.g., focus on embedded programs rather than on pure functional programs. 609 610 \item Implicit complexity programming languages are a straight jacket: {\bf restrictions} are often complex and too difficult to program with. 639 611 640 612 \end{itemize} 641 642 \noindent \Red{{\bf Our challenge}}643 Lift in a {\em certified way} whathever information we have on the execution644 cost of the binary code to an information on the $\C$ source code (a kind645 of {\bf decompilation}).646 613 647 614 \end{frame} … … 669 636 670 637 638 \begin{frame} 639 640 \frametitle{Current technology and our challenge (again)} 641 \begin{itemize} 642 643 644 \item Compilation phases are heavily {\bf inspected and tested} 645 but not formally checked with a proof assistant. 646 \[ 647 \lustre \arrow \C \arrow \textsc{binary~ code} 648 \] 649 \item Binary code must be {\bf annotated} with (uncertified) 650 information on the number of iterations of loops. 651 652 \item Tools such as \textsc{AbsInt} perform WCET analysis of 653 {\bf sequences of instructions of binary code}. 654 655 \end{itemize} 656 657 \noindent \Red{{\bf Our challenge}} 658 Lift in a {\em certified way} whathever information we have on the execution 659 cost of the binary code to an information on the $\C$ source code (a kind 660 of {\bf decompilation}). 661 662 \end{frame} 663 664 665 666 671 667 672 668 \begin{frame}
Note: See TracChangeset
for help on using the changeset viewer.