708 \begin{frame}[c] |
708 \begin{frame}[c] |
709 \frametitle{Midway Conclusion}% |
709 \frametitle{Midway Conclusion}% |
710 |
710 |
711 \begin{itemize} |
711 \begin{itemize} |
712 \item feels awfully like reasoning about machine code |
712 \item feels awfully like reasoning about machine code |
713 \item compositional constructions / reasoning not frictionless |
713 \item compositional constructions / reasoning not at all frictionless |
714 \item sizes |
714 \item sizes |
715 |
715 |
716 \begin{center} |
716 \begin{center} |
717 \begin{tabular}{ll} |
717 \begin{tabular}{ll} |
718 & sizes:\smallskip\\ |
718 & sizes:\smallskip\\ |
719 UF & 140843 constructors\\ |
719 UF & 140843 constructors\\ |
720 Reg.~Mach.~ & @{text 2} Mio instructions\\ |
720 URM & @{text 2} Mio instructions\\ |
721 UTM & @{text 38} Mio states\\ |
721 UTM & @{text 38} Mio states\\ |
722 \end{tabular} |
722 \end{tabular} |
723 \end{center}\pause |
723 \end{center}\smallskip\pause |
724 |
724 |
725 \item an observation: our treatment of recursive functions is a mini-version |
725 \item an observation: our treatment of recursive functions is a mini-version |
726 of the work by\\ Myreen \& Owens about deeply embedding HOL |
726 of the work by\\ Myreen \& Owens about deeply embedding HOL |
727 \end{itemize} |
727 \end{itemize} |
728 |
728 |
729 \only<1>{ |
729 \only<1>{ |
730 \begin{textblock}{4}(2,13.9) |
730 \begin{textblock}{4}(2,13.9) |
731 \begin{tikzpicture} |
731 \begin{tikzpicture} |
732 \draw (0,0) node {\small\begin{tabular}{l}$^\star$old version: |
732 \draw (0,0) node {\small\begin{tabular}{l}$^\star$old version: |
733 RM (@{text 12} Mio) UTM (@{text 112} Mio)\end{tabular}}; |
733 URM (@{text 12} Mio) UTM (@{text 112} Mio)\end{tabular}}; |
734 \end{tikzpicture} |
734 \end{tikzpicture} |
735 \end{textblock}} |
735 \end{textblock}} |
736 |
736 |
737 \end{frame}} |
737 \end{frame}} |
738 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
738 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
739 *} |
739 *} |
740 |
740 |
|
741 text_raw {* |
|
742 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
743 \mode<presentation>{ |
|
744 \begin{frame}[c] |
|
745 \frametitle{\begin{tabular}{@ {}c@ {}}Stealing From Other Works\end{tabular}}% |
|
746 |
|
747 \begin{itemize} |
|
748 \item Jensen, Benton, Kennedy ({\bf 2013}), |
|
749 {\it High-Level Separation Logic for Low-Level Code}\medskip\\ |
|
750 |
|
751 \item Myreen ({\bf 2008}), {\it Formal Verification of Machine-Code Programs}, |
|
752 PhD thesis\medskip |
|
753 |
|
754 \item Klein, Kolanski, Boyton ({\bf 2012}), {\it Mechanised Separation Algebra} |
|
755 |
|
756 \end{itemize} |
|
757 \end{frame}} |
|
758 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
759 *} |
|
760 |
|
761 text_raw {* |
|
762 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
763 \mode<presentation>{ |
|
764 \begin{frame}[c] |
|
765 \frametitle{Better Composability}% |
|
766 |
|
767 \begin{itemize} |
|
768 \item an idea from Jensen, Benton, Kennedy who looked at X86 |
|
769 assembly programs and macros\bigskip |
|
770 |
|
771 \item assembly for TMs:\medskip |
|
772 \begin{center} |
|
773 \begin{tabular}{l} |
|
774 @{text "move_one_left"} @{text "\<equiv>"}\\ |
|
775 \hspace{13mm} @{text "\<Lambda> exit."}\\ |
|
776 \hspace{16mm} @{text "Inst (L, exit) (L, exit)"} @{text ";"}\\ |
|
777 \hspace{16mm} @{text "Label exit"}\\ |
|
778 \end{tabular} |
|
779 \end{center}\bigskip\bigskip |
|
780 |
|
781 \begin{tabular}{l} |
|
782 $\Rightarrow$ represent "state" labels as functions\\ |
|
783 \phantom{$\Rightarrow$} (with bound variables $\Rightarrow$ locality) |
|
784 \end{tabular} |
|
785 \end{itemize} |
|
786 \end{frame}} |
|
787 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
788 *} |
|
789 |
|
790 text_raw {* |
|
791 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
792 \mode<presentation>{ |
|
793 \begin{frame}[c] |
|
794 \frametitle{Better Composability}% |
|
795 |
|
796 \begin{center} |
|
797 \begin{tabular}{@ {\hspace{-10mm}}l} |
|
798 @{text "move_left_until_zero"} @{text "\<equiv>"} \\ |
|
799 \hspace{31mm} @{text "\<Lambda> start exit."}\\ |
|
800 \hspace{36mm} @{text "Label start"} @{text ";"}\\ |
|
801 \hspace{36mm} @{text "if_zero exit"} @{text ";"}\\ |
|
802 \hspace{36mm} @{text "move_left"} @{text ";"}\\ |
|
803 \hspace{36mm} @{text "jmp start"} @{text ";"}\\ |
|
804 \hspace{36mm} @{text "Label exit"}\\ |
|
805 \end{tabular} |
|
806 \end{center} |
|
807 |
|
808 \small |
|
809 \begin{tabular}{l} |
|
810 @{text "if_zero e \<equiv> \<Lambda> exit. Inst (W\<^isub>0, e), (W\<^isub>1, exit); Label exit"}\\ |
|
811 \hspace{5mm}@{text "jmp e \<equiv> Inst (W\<^isub>0, e), (W\<^isub>1, e)"} |
|
812 \end{tabular} |
|
813 |
|
814 \end{frame}} |
|
815 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
816 *} |
|
817 |
|
818 text_raw {* |
|
819 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
820 \mode<presentation>{ |
|
821 \begin{frame}[c] |
|
822 \frametitle{{\large The Trouble With Hoare-Triples}}% |
|
823 |
|
824 \begin{itemize} |
|
825 \item Whenever we wanted to prove |
|
826 |
|
827 \begin{center} |
|
828 \large @{text "{P} p {Q}"} |
|
829 \end{center}\bigskip\medskip |
|
830 |
|
831 \item[@{text "(1)"}] we had to find a termination order proving that @{text p} terminates |
|
832 \textcolor{gray}{(not easy)} |
|
833 |
|
834 \item[@{text "(2)"}] we had to find invariants for each state\\ \textcolor{gray}{(not easy either)} |
|
835 \end{itemize}\pause |
|
836 |
|
837 \begin{center} |
|
838 \alert{very little opportunity for automation} |
|
839 \end{center} |
|
840 |
|
841 \end{frame}} |
|
842 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
843 *} |
741 |
844 |
742 text_raw {* |
845 text_raw {* |
743 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
846 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
744 \mode<presentation>{ |
847 \mode<presentation>{ |
745 \begin{frame}[c] |
848 \begin{frame}[c] |
746 \frametitle{Separation Algebra}% |
849 \frametitle{Separation Algebra}% |
747 |
850 |
748 \begin{itemize} |
851 \begin{itemize} |
749 \item introduced a separation algebra framework for register machines and TMs |
852 \item use some infrastructure introduced by Klein et al in Isabelle/HOL |
750 \item we can semi-automate the reasoning for our small TMs |
853 \item and an idea by Myreen\bigskip\bigskip |
751 \item we can assemble bigger programs out of smaller components\bigskip |
854 |
752 |
855 \begin{center} |
753 \item looks awfully like ``real'' assembly code\pause |
856 \large @{text "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"}\bigskip\bigskip |
754 \item Conclusion: we have a playing ground for reasoning about low-level |
857 \end{center} |
755 code; we work on automation |
858 |
756 \end{itemize} |
859 \item[] @{text "p, c, q"} will be assertions in a separation logic\pause |
757 \end{frame}} |
860 |
758 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
861 \begin{center} |
759 *} |
862 e.g.~~@{text "\<lbrace>st i \<star> hd n \<star> ones u v \<star> zero (v + 1)\<rbrace>"} |
760 |
863 \end{center} |
761 |
864 \end{itemize} |
762 |
865 \end{frame}} |
|
866 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
867 *} |
|
868 |
|
869 text_raw {* |
|
870 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
871 \mode<presentation>{ |
|
872 \begin{frame}[c] |
|
873 \frametitle{Separation Triples}% |
|
874 |
|
875 \Large |
|
876 \begin{center} |
|
877 \begin{tabular}{l@ {\hspace{-10mm}}l} |
|
878 @{text "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"} @{text "\<equiv>"}\smallskip\\ |
|
879 & @{text "\<forall> cf r."}\\ |
|
880 & \hspace{3mm} @{text "(p \<star> c \<star> r) cf"} implies\\ |
|
881 & \hspace{3mm} @{text "\<exists> k. "} @{text "(q \<star> c \<star> r) (run k cf)"} |
|
882 \end{tabular} |
|
883 \end{center}\bigskip\bigskip |
|
884 |
|
885 \normalsize |
|
886 @{text "c"} can be\;\;\; @{text "i:[move_left_until_zero]:j"} |
|
887 |
|
888 |
|
889 \end{frame}} |
|
890 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
891 *} |
|
892 |
|
893 text_raw {* |
|
894 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
895 \mode<presentation>{ |
|
896 \begin{frame}[c] |
|
897 \frametitle{Automation}% |
|
898 |
|
899 \begin{itemize} |
|
900 \item we introduced some tactics for handling sequential programs\bigskip |
|
901 |
|
902 \begin{center} |
|
903 @{text "\<lbrace>p\<rbrace> i:[c\<^isub>1 ; ... ; c\<^isub>n]:j \<lbrace>q\<rbrace>"} |
|
904 \end{center}\bigskip\bigskip |
|
905 |
|
906 \item for loops we often only have to do inductions on the length |
|
907 of the input (e.g.~how many @{text "1"}s are on the tape)\pause |
|
908 |
|
909 \item these macros allow us to completely get rid of register machines |
|
910 \end{itemize} |
|
911 |
|
912 |
|
913 \end{frame}} |
|
914 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
915 *} |
|
916 |
|
917 text_raw {* |
|
918 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
919 \mode<presentation>{ |
|
920 \begin{frame}[c] |
|
921 \frametitle{Conclusion}% |
|
922 |
|
923 \begin{itemize} |
|
924 \item What started out as a student project, turned out to be much more |
|
925 fun than first thought.\bigskip |
|
926 |
|
927 \item Where can you claim that you proved the correctness of |
|
928 a @{text "38"} Mio instruction program. |
|
929 (ca.~@{text 7000} is the soa \raisebox{-1mm}{\includegraphics[scale=0.077]{smiley.jpg}}) |
|
930 \bigskip |
|
931 |
|
932 \item We learned a lot about current verification technology for low-level code. |
|
933 \end{itemize} |
|
934 |
|
935 |
|
936 \end{frame}} |
|
937 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
938 *} |
763 |
939 |
764 (*<*) |
940 (*<*) |
765 end |
941 end |
766 end |
942 end |
767 (*>*) |
943 (*>*) |