Changeset 3287
- Timestamp:
- May 14, 2013, 3:58:12 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/Dissemination/back-end/back-end.tex
r3281 r3287 491 491 \item The issues with defining a good $S$ are no different than in extensional proofs 492 492 \item $C$ is defined based on program counters only 493 \item The Matita proof is \structure{complete} 493 494 \end{itemize} 494 495 \end{frame} … … 685 686 \end{columns} 686 687 \end{frame} 687 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 688 \begin{frame}% 689 %[] 688 \section{Details on the passes} 689 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 690 \begin{frame}% 691 %[] 692 \frametitle{RTLabs $\to$ RTL} 693 \begin{itemize} 694 \item Most of the effort must go to the \structure{extensional} part, as multi-byte operations 695 are replaced by sequences of single byte operations 696 \item Status: sketched 697 \end{itemize} 698 \end{frame} 699 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 700 \begin{frame}% 701 %[] 702 \frametitle{RTL $\to$ ERTL} 703 \begin{itemize} 704 \item A \structure{graph} pass 705 \item Implements the calling convention, with the first accesses to stack 706 \item From the intensional point of view: calls have prefixes and suffixes, and 707 function bodies have preambles 708 \item Status: the scaffolding underlying all graph passes 709 is done. The proof obligations regarding this particular pass are open 710 \end{itemize} 711 \end{frame} 712 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 713 \begin{frame}% 714 %[] 715 \frametitle{ERTL $\to$ LTL} 716 \begin{itemize} 717 \item A \structure{graph} pass 718 \item Register allocation, spilling, saving and restoring callee-saved hardware registers 719 \item From the intensional point of view, calls to pointer have prefixes, and 720 function bodies have preambles 721 \item Status: the scaffolding underlying all graph passes 722 is done. The proof obligations regarding this particular pass are almost finished 723 \end{itemize} 724 \end{frame} 725 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 726 \begin{frame}% 727 %[] 728 \frametitle{LTL $\to$ LIN} 729 \begin{itemize} 730 \item A \structure{linearisation} 731 \item From the intensional point of view, calls can have suffixes (GOTOs) 732 \item Status: the generic linearisation scaffolding is complete. 733 The proof obligations regarding this particular pass are open (but easy) 734 \end{itemize} 735 736 \end{frame} 737 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 738 \begin{frame}% 739 %[] 740 \frametitle{LIN $\to$ ASM} 741 \begin{itemize} 742 \item A 1-to-1 simulation 743 \item Function names and code labels are collapsed in the same global namespace 744 \item Status: open 745 \end{itemize} 746 \end{frame} 747 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 748 690 749 \section{Assembler correctness} 691 750 751 \begin{frame}% 752 %[] 692 753 \frametitle{Assembler correctness} 693 754 Assembler outputs \structure{labelled} object code and the \structure{cost map}
Note: See TracChangeset
for help on using the changeset viewer.