# HG changeset patch # User Christian Urban # Date 1374563194 -7200 # Node ID 42f2c28d1ce6a78dafeb687ef83eeae105031b36 # Parent 4457185b22ef4b15fc5c1c70ee7a48ef6e50f213 new verison of the slides diff -r 4457185b22ef -r 42f2c28d1ce6 README --- a/README Wed Jul 17 10:33:19 2013 +0100 +++ b/README Tue Jul 23 09:06:34 2013 +0200 @@ -29,4 +29,11 @@ isabelle build -d . UTM isabelle make utm -- creates the big session file -isabelle make itp -- creates paper \ No newline at end of file +isabelle make itp -- creates paper + + + +============================ +ROOT setup + +isabelle build -d . Slides2 \ No newline at end of file diff -r 4457185b22ef -r 42f2c28d1ce6 ROOT --- a/ROOT Wed Jul 17 10:33:19 2013 +0100 +++ b/ROOT Tue Jul 23 09:06:34 2013 +0200 @@ -25,4 +25,4 @@ session Slides2 in Slides = UTM + options [document = pdf, document_output = "..", document_variants = "slides2"] theories - "Slides2" \ No newline at end of file + "Slides2" diff -r 4457185b22ef -r 42f2c28d1ce6 Slides/Slides2.thy --- a/Slides/Slides2.thy Wed Jul 17 10:33:19 2013 +0100 +++ b/Slides/Slides2.thy Tue Jul 23 09:06:34 2013 +0200 @@ -11,10 +11,11 @@ notation (latex output) - Cons ("_::_" [48,47] 48) and + Cons ("_::_" [48,47] 68) and + append ("_@_" [65, 64] 65) and Oc ("1") and Bk ("0") and - exponent ("_\<^bsup>_\<^esup>") and + exponent ("_\<^bsup>_\<^esup>" [107] 109) and inv_begin0 ("I\<^isub>0") and inv_begin1 ("I\<^isub>1") and inv_begin2 ("I\<^isub>2") and @@ -86,38 +87,50 @@ \frametitle{% \begin{tabular}{@ {}c@ {}} \\[-3mm] - \Large Reasoning about Turing Machines\\[-1mm] - \Large and Low-Level Code\\[-3mm] + {\fontsize{20}{20}\selectfont{}Mechanising Turing Machines and}\\[-2mm] + {\fontsize{20}{20}\selectfont{}Computability Theory in Isabelle}\\[-3mm] \end{tabular}} - \begin{center} - Christian Urban\\[1mm] - %%\small King's College London - \end{center}\bigskip + \bigskip\medskip\medskip \begin{center} - in cooperation with Jian Xu and Xingyuan Zhang + \begin{tabular}{c@ {\hspace{1cm}}c} + \includegraphics[scale=0.29]{jian.jpg} & + \includegraphics[scale=0.034]{xingyuan.jpg} \\ + Jian Xu & Xingyuan Zhang\\[-3mm] + \end{tabular}\\[3mm] + \small PLA University of Science and Technology + \end{center} + + \begin{center} + Christian Urban\\[0mm] + \small King's College London \end{center} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} + text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}[c] - \frametitle{A Trend in Verification}% + \frametitle{Why Turing Machines?}% \begin{itemize} - \item in the past:\\ - \begin{quote} - model a problem mathematically and proof properties about the - model - \end{quote}\bigskip + \item At the beginning, it was just a student project + about computability.\smallskip - \item needs elegance, is still very hard\bigskip\pause + \begin{center} + \begin{tabular}{c} + \includegraphics[scale=0.3]{boolos.jpg}\\[-2mm] + \footnotesize Computability and Logic (5th.~ed)\\[-2mm] + \footnotesize Boolos, Burgess and Jeffrey\\[2mm] + \end{tabular} + \end{center} - \item does not help with ensuring the correctness of running programs + \item found an inconsistency in the definition of halting computations + (Chap.~3 vs Chap.~8) \end{itemize} \end{frame}} @@ -128,60 +141,23 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}[c] - \frametitle{A Trend in Verification}% - - \begin{itemize} - \item make the specification executable (e.g.~Compcert)\bigskip\pause - - you would expect the trend would be to for example model C, implement - your programs in C and verify the programs written in C (e.g.~seL4) - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{A Trend in Verification}% + \frametitle{Some Previous Work}% \begin{itemize} - \item but actually people start to verify machine code directly - (e.g.~bignum arithmetic implemented in x86-64 -- 700 instructions) - - \item CPU models exists, but the strategy is to use a small subset - which you use in your programs + \item Norrish formalised computability theory in HOL starting + from the lambda-calculus + \begin{itemize} + \item \textcolor{gray}{for technical reasons we could not follow him} + \item \textcolor{gray}{some proofs use TMs (Wang tilings)} \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Why Turing Machines}% + - \begin{itemize} - \item at the beginning it was just a nice student project - about computability - \begin{center} - \includegraphics[scale=0.3]{boolos.jpg} - \end{center} + \bigskip - \item found an inconsistency in the definition of halting computations - (Chap.~3 vs Chap.~8) - \pause - - \item \small Norrish formalised computability via lambda-calculus (and nominal); - Asperti and Riccioti formalised TMs but didn't get proper UTM + \item Asperti and Ricciotti formalised TMs in Matita \end{itemize} - \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} @@ -193,7 +169,7 @@ \frametitle{Turing Machines}% \begin{itemize} - \item tapes contain 0 or 1 only + \item tapes are lists and contain @{text 0}s or @{text 1}s only \begin{center} \begin{tikzpicture}[scale=1] @@ -222,13 +198,39 @@ \end{tikzpicture} \end{center} - \item steps function + \item @{text steps} function: - \begin{quote} - What does the tape look like after the TM has executed n steps? + \begin{quote}\rm + What does the TM claclulate after it has executed @{text n} steps? \end{quote}\pause - designate the 0-state as halting state and remain there forever + \item designate the @{text 0}-state as \"halting state\" and remain there + forever, i.e.~have a @{text Nop}-action + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{Register Machines}% + + \begin{itemize} + \item instructions + + \begin{center} + \begin{tabular}{rcl@ {\hspace{10mm}}l} + @{text "I"} & $::=$ & @{term "Inc R\"} & increment register @{text "R"} by one\\ + & $\mid$ & @{term "Dec R\ L\"} & if content of @{text R} is non-zero,\\ + & & & then decrement it by one\\ + & & & otherwise jump to instruction @{text L}\\ + & $\mid$ & @{term "Goto L\"} & jump to instruction @{text L} + \end{tabular} + \end{center} + \end{itemize} \end{frame}} @@ -250,9 +252,9 @@ \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$}; \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$}; \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$}; - \node [anchor=base] at (2.2,-0.8) {\small$\overbrace{\text{cbegin}}^{}$}; - \node [anchor=base] at (5.6,-0.8) {\small$\overbrace{\text{cloop}}^{}$}; - \node [anchor=base] at (10.5,-0.8) {\small$\overbrace{\text{cend}}^{}$}; + \node [anchor=base] at (2.2,-0.8) {\small$\overbrace{@{text cbegin}}^{}$}; + \node [anchor=base] at (5.6,-0.8) {\small$\overbrace{@{text cloop}}^{}$}; + \node [anchor=base] at (10.5,-0.8) {\small$\overbrace{@{text cend}}^{}$}; \begin{scope}[shift={(0.5,0)}] @@ -405,11 +407,13 @@ \frametitle{Hoare Reasoning}% \begin{itemize} - \item reasoning is still quite difficult---invariants + \item reasoning is still quite demanding;\\ + the invariants of the copy-machine:\\[-5mm]\mbox{} \footnotesize \begin{center} -\begin{tabular}{@ {\hspace{-4mm}}lcl@ {\hspace{-0.9cm}}l@ {}} + \begin{tabular}{@ {\hspace{-5mm}}c@ {}} + \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {\hspace{-0.9cm}}l@ {}} \hline @{thm (lhs) inv_begin1.simps} & @{text "\"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\ @{thm (lhs) inv_begin2.simps} & @{text "\"} & @{thm (rhs) inv_begin2.simps}\\ @@ -426,6 +430,7 @@ @{thm (lhs) inv_end0.simps} & @{text "\"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\ \hline \end{tabular} + \end{tabular} \end{center} \end{itemize} @@ -434,30 +439,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Register Machines}% - \begin{itemize} - \item instructions - - \begin{center} - \begin{tabular}{rcl@ {\hspace{10mm}}l} - @{text "I"} & $::=$ & @{term "Inc R\"} & increment register @{text "R"} by one\\ - & $\mid$ & @{term "Dec R\ L\"} & if content of @{text R} is non-zero,\\ - & & & then decrement it by one\\ - & & & otherwise jump to instruction @{text L}\\ - & $\mid$ & @{term "Goto L\"} & jump to instruction @{text L} - \end{tabular} - \end{center} - - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -486,13 +468,13 @@ \frametitle{Sizes}% \begin{itemize} - \item UF (size: 140843) - \item Register Machine (size: 2 Mio instructions) - \item UTM (size: 38 Mio states) + \item UF (size: @{text 140843}) + \item Register Machine (size: @{text 2} Mio instructions) + \item UTM (size: @{text 38} Mio states) \end{itemize}\bigskip\bigskip \small - old version: RM (12 Mio) UTM (112 Mio) + old version: RM (@{text 12} Mio) UTM (@{text 112} Mio) \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} diff -r 4457185b22ef -r 42f2c28d1ce6 Slides/document/jian.jpg Binary file Slides/document/jian.jpg has changed diff -r 4457185b22ef -r 42f2c28d1ce6 slides2.pdf Binary file slides2.pdf has changed