1\hypersetup{% 2 pdfauthor={Thomas~Tuerk} 3 pdftitle={Deep Embeeding of Separation Logic} 4} 5 6\title[Deep Embeeding of Separation Logic]{A Deep Embedding of a \\Decidable Fragment of Separation Logic in HOL} 7\author[Tuerk, Gordon]{Thomas Tuerk \and Mike Gordon} 8\date{ARG Lunch, 26th June 2006} 9 10\newcommand{\smallfoot}{{\sf Smallfoot}} 11\newcommand{\HOL}{{\sf HOL}} 12\newcommand{\nil}{{\textsf{nil}}} 13\newcommand{\pftrue}{{\textsf{true}}} 14\newcommand{\pfequal}[2]{\ensuremath{#1 \doteq #2}} 15\newcommand{\pfunequal}[2]{\ensuremath{#1 \not\doteq #2}} 16\newcommand{\values}{{\emph{Values}}} 17\newcommand{\valuesnil}{\ensuremath{\values_\nil}} 18\newcommand{\vars}{{\emph{Vars}}} 19\newcommand{\expr}{{\emph{Exp}}} 20\newcommand{\fields}{{\emph{Fields}}} 21\newcommand{\pf}{{\emph{pf}}} 22\newcommand{\sfset}{{\emph{sf}}} 23\newcommand{\modelspf}{{\models_{\textit{pf}}\ }} 24\newcommand{\modelssf}{{\models_{\textit{sf}}\ }} 25\newcommand{\modelsds}{{\models_{\textit{ds}}\ }} 26 27 28\newcommand{\sfemp}{{\textsf{emp}}} 29\newcommand{\sftree}{{\textsf{tree}}} 30\newcommand{\sfpointsto}[2]{#1 \hookrightarrow [#2]} 31\newcommand{\sfbintree}{{\textsf{bin-tree}}} 32\newcommand{\sflist}{{\textsf{ls}}} 33 34\newcommand{\varpf}[1]{\textit{pf}_{#1}} 35\newcommand{\varsf}[1]{\textit{sf}_{#1}} 36\newcommand{\varel}{\eta} 37\newcommand{\varepl}{\pi} 38 39\newcommand{\heapdistinct}{\textit{heap\_distinct}} 40\newcommand{\entailment}[2]{#1\ \vdash\ #2} 41\newcommand{\dom}{{\text{dom}}} 42\newcommand{\tofin}{\xrightarrow{fin}} 43 44\newcommand{\eqinferstyle}{ 45\mprset{fraction={={\raisebox{0pt}[5pt][5pt]{=}}=}}} 46 47 48\begin{document} 49 50\frame{\titlepage} 51 52\frame{\frametitle{Overview}\tableofcontents[hideallsubsections]} 53 54\section{Motivation} 55\subsection*{} 56 57\begin{frame} 58\frametitle{Smallfoot} 59\begin{itemize} 60\item "\smallfoot\ is an automatic verification tool which checks separation 61logic specifications of concurrent programs which manipulate 62dynamically-allocated recursive data structures." (\smallfoot\ documentation) 63\item developed by 64\begin{itemize} 65\item Cristiano Calcagno 66\item Josh Berdine 67\item Peter O'Hearn 68\end{itemize} 69\end{itemize} 70\end{frame} 71 72\begin{frame}[fragile] 73\frametitle{Smallfoot II} 74 75\begin{exampleblock}{Example from \texttt{list.sf}} 76\begin{semiverbatim} 77list_copy(p) [list(p)] \{ 78 local t; 79 t = p; 80 q = NULL; 81 while(t != NULL) [list(q) * lseg(p,t) * list(t)] \{ 82 sq = q; 83 q = new(); 84 q->tl = sq; 85 t = t->tl; 86 \} 87\} [list(p) * list(q)] 88\end{semiverbatim} 89\end{exampleblock} 90\end{frame} 91 92 93\begin{frame} 94\frametitle{Motivation} 95\begin{itemize} 96\item we deeply embedded the fragment of separation logic used by \smallfoot\ 97 in \HOL 98\item a decision procedure for entailments has been implemented in \HOL 99\item this formalisation may increase the trust in \smallfoot 100\item it may be used as a basis for non decidable fragments of separation 101 logic and an interactive proof environment 102\item it may be extended to a \HOL\ implementation of \smallfoot 103\end{itemize} 104\end{frame} 105 106 107\section{Basic Definitions} 108\subsection*{} 109 110\begin{frame} 111\frametitle{Pure Formulae} 112\begin{itemize} 113\item an \alert{expression} is either a constant or a variable 114\item \alert{nil} is a special constant 115\item a \alert{stack} is a variable assignment 116\item \alert{pure formulae} are inductively defined by 117\begin{itemize} 118\item $\pftrue$ 119\item $\pfequal {e_1} {e_2}$, $\pfunequal {e_1} {e_2}$ 120\item $pf_1 \wedge pf_2$ 121\end{itemize} 122\item the semantics of pure formulae with respect to a stack are defined in 123 the natural way 124\end{itemize} 125\end{frame} 126 127 128\begin{frame} 129\frametitle{Spatial Formulae} 130\begin{itemize} 131\item a \alert{heap} is finite map $h : (Values \setminus \{nil\}) \tofin Fields \tofin Values$ 132\item \alert{spatial formulae} are inductively defined by 133\begin{itemize} 134\item $\sfemp$ 135\item $\sfpointsto {e} {t_1:e_1, \ldots, t_n : e_n}$ 136\item $sf_1 * sf_2$ 137\item $\sftree((t_1, \ldots, t_n), es, e)$ 138\end{itemize} 139\item list segments and binary trees are defined as syntactic sugar 140\begin{itemize} 141\item $\sfbintree(l, r, e) := \sftree((l,r), nil, e)$ 142\item $\sflist(tl, e_1, e_2) := \sftree(tl, e_2, e_1)$ 143\end{itemize} 144\end{itemize} 145\end{frame} 146 147 148\begin{frame} 149\frametitle{Spatial Formulae II} 150\begin{columns}[c] 151\begin{column}{0.2\textwidth} 152\begin{pgfpicture}{0cm}{0cm}{1.5 cm}{2cm} 153 \color{black} 154 \color<7->{alert} 155 \pgfcircle[fill]{\pgfxy(1,0)}{0.2 cm} 156 \pgfcircle[fill]{\pgfxy(0,0)}{0.2 cm} 157 158 159 160 \color<6->{alert} 161 \pgfsetendarrow{\pgfarrowtriangle{2pt}} 162 163 \pgfline{\pgfxy(0.6,0.8)}{\pgfxy(0.9,0.2)} 164 \pgfline{\pgfxy(0.4,0.8)}{\pgfxy(0.1,0.2)} 165 166 167 \pgfputat{\pgfxy(0.1,0.6)}{\pgfbox[center,center]{l}} 168 \pgfputat{\pgfxy(0.9,0.6)}{\pgfbox[center,center]{r}} 169 170 \pgfcircle[stroke]{\pgfxy(0.5,1)}{0.2 cm} 171 \pgfputat{\pgfxy(0.5,1)}{\pgfbox[center,center]{2}} 172 173 174 \color<5->{alert} 175 \pgfcircle[fill]{\pgfxy(1.5,1)}{0.2 cm} 176 177 178 179 \color<4->{alert} 180 \pgfputat{\pgfxy(0.6,1.6)}{\pgfbox[center,center]{l}} 181 \pgfputat{\pgfxy(1.4,1.6)}{\pgfbox[center,center]{r}} 182 183 \pgfline{\pgfxy(0.9,1.8)}{\pgfxy(0.6,1.2)} 184 \pgfline{\pgfxy(1.1,1.8)}{\pgfxy(1.4,1.2)} 185 186 187 \pgfcircle[stroke]{\pgfxy(1,2)}{0.2 cm} 188 \pgfputat{\pgfxy(1,2)}{\pgfbox[center,center]{1}} 189 190 191\end{pgfpicture} 192\end{column} 193\begin{column}{0.8\textwidth} 194$s (x_i) := i$\\ 195$\alert<7->{h := [\alert<4->{1 \to [l \to 2, r \to nil]}, \alert<6->{2 \to [l \to nil, r \to nil]}]}$ 196\end{column} 197\end{columns} 198\bigskip 199\bigskip 200\begin{center} 201\only<1>{{$\sfbintree(l,r,x_1)$}} 202\only<2>{{$\sftree((l,r),\nil,x_1)$}} 203\only<3>{{$\exists e_l, e_r. \ \sfpointsto{x_1} {l:e_l, r:e_r} * 204 \sftree((l,r),\nil,e_l) * \sftree((l,r),\nil,e_r)$}} 205\only<4>{{$\alert{\sfpointsto{x_1} {l:2, r:\nil}} * \sftree((l,r),\nil,2) * 206 \sftree((l,r),\nil,\nil)$}} 207\only<5>{{$\alert{\sfpointsto{x_1} {l:2, r:\nil}} * \sftree((l,r),\nil,2) 208 * \alert{\sftree((l,r),\nil,\nil)}$}} 209\only<6>{{$\alert{\sfpointsto{x_1} {l:2, r:\nil}} * \alert{\sfpointsto{2} 210 {l:\nil, r:\nil}}\ *$ $\sftree((l,r),\nil,\nil) * 211 \sftree((l,r),\nil,\nil) * \alert{\sftree((l,r),\nil,\nil)}$}} 212\only<7>{\alert{$\sfpointsto{x_1} {l:2, r:\nil} * \sfpointsto{2} 213 {l:\nil, r:\nil}\ *$ $\sftree((l,r),\nil,\nil) * 214 \sftree((l,r),\nil,\nil) * \sftree((l,r),\nil,\nil)$}} 215\end{center} 216\end{frame} 217 218\section[Entailments]{A Decision Procedure for Entailments} 219\subsection*{} 220 221\begin{frame}[fragile] 222\frametitle{Entailments} 223 224\begin{itemize} 225\item entailments are important for \smallfoot 226\item example from \texttt{list.sf} 227\[\small\begin{array}{lr} 228\pfunequal {x_0} \nil,\pfunequal {x_1} \nil, \pfunequal {x_2} \nil, 229\pfunequal {x_0} {x_3}, \pfunequal {x_0} {x_2}, \pfunequal {x_4} {x_5},\\ 230\pfunequal {x_1} {x_3}, 231\pfunequal {x_1} {x_2}, \pfunequal {x_3} {x_2},\\ 232\sfpointsto {x_2} {\textit{hd}:x_5, \textit{tl}:x_3}, 233\sflist(\textit{tl},x_3,\nil), \sflist(\textit{tl},x_1,x_0), 234\sfpointsto {x_0} {\textit{tl},x_2} & \vdash \\ 235\sflist(\textit{tl},x_1,x_2), \sfpointsto {x_2} {\textit{tl}:x_3}, \sflist(\textit{tl},x_3,\nil) 236\end{array} 237\] 238\item entailments in this fragment of separation logic are decidable 239\item inferences can be easily combined to form a decision procedure 240\item inferences and decision procedure are presented in 241\begin{semiverbatim}\small 242Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. 243Symbolic Execution with Separation Logic. 244In K. Yi (Ed.): APLAS 2005, LNCS 3780, pp. 52-68, 2005. 245\end{semiverbatim} 246\end{itemize} 247\end{frame} 248 249\begin{frame} 250\frametitle{\textsf{RemoveTrivial}} 251\small\[\begin{array}{l} 252\inferrule[RemoveTrivial-EQ-L]{\entailment{\Pi,\Sigma}{\Pi',\Sigma'}} 253{\entailment{\alert{\pfequal e e},\Pi,\Sigma}{\Pi', \Sigma'}} 254\bigskip\\ 255\inferrule[RemoveTrivial-EQ-R]{\entailment{\Pi,\Sigma}{\Pi',\Sigma'}} 256{\entailment{\Pi,\Sigma}{\alert{\pfequal e e}, \Pi', \Sigma'}} 257\bigskip\\ 258\inferrule[RemoveTrivial-EmpTree-L]{\entailment{\Pi,\Sigma}{\Pi',\Sigma'}} 259{\entailment{\Pi,\alert{\sftree((t_1, \ldots, t_k),e,e)},\Sigma}{\Pi', \Sigma'}} 260\bigskip\\ 261\inferrule[RemoveTrivial-EmpTree-R]{\entailment{\Pi,\Sigma}{\Pi',\Sigma'}} 262{\entailment{\Pi,\Sigma}{\Pi',\alert{\sftree((t_1, \ldots, t_k),e,e)}, \Sigma'}} 263\end{array} 264\] 265\end{frame} 266 267 268\begin{frame} 269\frametitle{\textsf{Hypothesis}} 270\small\[ 271\inferrule[Hypothesis]{\entailment{\alert{\varpf{}},\Pi,\Sigma}{\Pi',\Sigma'}} 272{\entailment{\alert{\varpf{}},\Pi,\Sigma}{\alert{\varpf {}},\Pi', \Sigma'}} 273\] 274\end{frame} 275 276\begin{frame} 277\frametitle{\textsf{Axiom / Inconsistent}} 278\small\[\begin{array}{ll} 279\inferrule[Axiom]{\ } 280{\entailment{\Pi}{\ }} 281\bigskip\\ 282\inferrule[Inconsistent-unequal] 283{\ } 284{\entailment{\alert{\pfunequal e e},\Pi,\Sigma}{\Pi',\Sigma'}} 285& 286\inferrule[Inconsistent-pointsto-nil] 287{\ } 288{\entailment{\Pi,\alert{\sfpointsto \nil {\ldots}}, \Sigma}{\Pi',\Sigma'}} 289\end{array} 290\] 291\end{frame} 292 293 294\begin{frame} 295\frametitle{\textsf{Frame}} 296\small 297\[ 298\inferrule[Frame-base]{\entailment{\Pi,\Sigma}{\Pi',\Sigma'}} 299{\entailment{\Pi,\alert{\varsf{}},\Sigma}{\Pi', \alert{\varsf{}},\Sigma'}} 300\] 301 302\begin{itemize} 303\item problem: this is a real implication, information is lost 304\item thus, order of inference application matters 305\item example: $\entailment{\alert{\sfpointsto e {f:e_1}}, \sfpointsto e 306 {g:e_2}}{\alert{\sfpointsto e {f:e_1}}}$ 307\item solution: add additional informations to entailments 308\end{itemize} 309\end{frame} 310 311\begin{frame} 312\frametitle{\textsf{Frame II}} 313\vspace{-1cm} 314\[\small\begin{array}{l} 315\eqinferstyle 316\inferrule[Frame-points\_to] 317{\entailment{\alert{e},\eta,\pi,\Pi,\Sigma}{\Pi',\Sigma'}} 318{\entailment{\eta,\pi,\Pi,\alert{\sfpointsto e {t_1:e_1, \ldots, 319 t_n:e_n}},\Sigma}{\Pi', \alert{\sfpointsto e {t_1:e_1, \ldots, 320 t_m:e_m}},\Sigma'}} 321m \leq n 322\bigskip\\ 323\eqinferstyle 324\inferrule[Frame-tree] 325{\entailment{\eta,\alert{(e,es)},\pi,\Pi,\Sigma}{\Pi',\Sigma'}} 326{\entailment{\eta,\pi,\Pi,\alert{\sftree((t_1, \ldots, t_k),es,e)},\Sigma}{\Pi', \alert{\sftree((t_1, \ldots, t_k),es,e)},\Sigma'}} 327\end{array} 328\] 329\begin{itemize} 330\item all used inferences are equivalences 331\item order of application does not matter 332\item continued applications of inferences will terminate 333\end{itemize} 334\end{frame} 335 336 337\begin{frame} 338\frametitle{\textsf{Substitution}} 339\[\small 340\eqinferstyle 341\inferrule[Substitution]{\entailment{\eta[e/x],\pi[e/x],\Pi[e/x],\Sigma[e/x]}{\Pi'[e/x],\Sigma'[e/x]}} 342{\entailment{\eta,\alert{\pfequal x e},\pi,\Pi,\Sigma}{\Pi', \Sigma'}} 343\] 344\end{frame} 345 346\begin{frame} 347\frametitle{\textsf{NIL-NOT-LVAL}} 348\[\small\begin{array}{l} 349\eqinferstyle 350\inferrule[NIL-NOT-LVAL-pointsto] 351{\entailment{\eta,\pi,\alert{\pfunequal e \nil}, \Pi,\alert{\sfpointsto e {\ldots}},\Sigma}{\Pi',\Sigma'}} 352{\entailment{\eta,\pi,\Pi,\alert{\sfpointsto e {\ldots}},\Sigma}{\Pi',\Sigma'}} 353\bigskip\\ 354\eqinferstyle 355\inferrule[NIL-NOT-LVAL-tree] 356{\entailment{\eta,\pi,\alert{\pfunequal e \nil}, \alert{\pfunequal e \textit{es}},\Pi,\alert{\sftree\left(\ldots,\textit{es},e\right)},\Sigma}{\Pi',\Sigma'}} 357{\entailment{\eta,\pi,\alert{\pfunequal e \textit{es}},\Pi,\alert{\sftree\left(\ldots,\textit{es},e\right)},\Sigma}{\Pi',\Sigma'}} 358\end{array} 359\] 360\begin{alertblock}{side condition} 361In order to prevent looping only new facts are added. 362\end{alertblock} 363\end{frame} 364 365 366\begin{frame} 367\frametitle{\textsf{Partial}} 368\[\small\begin{array}{l} 369\eqinferstyle 370\inferrule[Partial-pointsto-pointsto] 371{\entailment{\eta,\pi,\alert{\pfunequal {e_1} {e_2}}, \Pi,\alert{\sfpointsto 372 {e_1} {\ldots}},\alert{\sfpointsto {e_2} {\ldots}},\Sigma}{\Pi',\Sigma'}} 373{\entailment{\eta,\pi,\Pi,\alert{\sfpointsto {e_1} {\ldots}},\alert{\sfpointsto {e_2} 374 {\ldots}},\Sigma}{\Pi',\Sigma'}} 375\bigskip\\ 376\eqinferstyle 377\inferrule[Partial-pointsto-tree] 378{\entailment{\eta,\pi,\alert{\pfunequal {e_1} {e_2}}, \alert{\pfunequal {e_2} {e_3}}, 379 \Pi,\alert{\sfpointsto {e_1} {\ldots}},\alert{\sftree (\ldots, {e_3}, e_2)},\Sigma}{\Pi',\Sigma'}} 380{\entailment{\eta,\pi,\alert{\pfunequal {e_2} {e_3}},\Pi,\alert{\sfpointsto {e_1} {\ldots}},\alert{\sftree (\ldots, {e_3}, e_2)},\Sigma}{\Pi',\Sigma'}} 381\bigskip\\ 382\vdots 383\end{array} 384\] 385\begin{alertblock}{side condition} 386In order to prevent looping only new facts are added. 387\end{alertblock} 388\end{frame} 389 390 391\begin{frame} 392\frametitle{\textsf{Simple Unroll}} 393\vspace{-0.5cm} 394\[\small\begin{array}{l} 395\eqinferstyle 396\inferrule[Unroll-right-list] 397{\entailment{\alert{e_1},\eta,\pi,\alert{\pfunequal {e_1} {e_3}}, \Pi,\Sigma}{\Pi',\sflist(\textit{tl}, \alert{e_2}, e_3),\Sigma'}} 398{\entailment{\eta,\pi,\alert{\pfunequal {e_1} {e_3}}, \Pi,\alert{\sfpointsto{e_1} 399 {\textit{tl}:e_2, \ldots}}, \Sigma}{\Pi',\alert{\sflist(\textit{tl}, e_1, e_3)},\Sigma'}} 400\bigskip\\ 401\eqinferstyle 402\inferrule[Unroll-right-bintree] 403{\entailment{\alert{e},\eta,\pi, \Pi,\Sigma}{\Pi',\alert{\sfbintree(l,r, e_l)},\alert{\sfbintree(l,r, e_r)},\Sigma'}} 404{\entailment{\eta,\pi,\Pi,\alert{\sfpointsto{e} 405 {l:e_l, r:e_r, \ldots}}, \Sigma}{\Pi',\alert{\sfbintree(l,r,e)},\Sigma'}} 406\bigskip\\ 407\eqinferstyle 408\inferrule[Unroll-NilList] 409{\entailment{\eta,\pi,\alert{\pfequal {e} {\nil}}, \Pi,\Sigma}{\Pi',\Sigma'}} 410{\entailment{\eta,\pi,\Pi,\alert{\sflist(\textit{tl}, \nil, e)},\Sigma}{\Pi',\Sigma'}} 411\bigskip\\ 412\eqinferstyle 413\inferrule[Unroll-precond-list] 414{\entailment{\alert{e_1},\eta,\pi,\alert{\pfequal {e_1} {e_2}}, \Pi,\Sigma}{\Pi',\Sigma'}} 415{\entailment{\alert{e_1},\eta,\pi,\Pi,\alert{\sflist(\textit{tl}, e_1, e_2)},\Sigma}{\Pi',\Sigma'}} 416\end{array} 417\] 418\end{frame} 419 420\begin{frame} 421\frametitle{\textsf{Unroll}} 422\[\small 423\eqinferstyle 424\inferrule[Unroll-list] 425{\entailment{\eta,\pi,\alert{\pfequal {e_1} {e_2}}, \Pi,\Sigma}{\Pi',\Sigma'} \\\\ 426 \alert{\forall x.}\ \entailment{\eta,\pi,\alert{\pfunequal {e_1} {e_2}},\alert{\pfunequal {e_2} {x}}, 427 \Pi,\alert{\sfpointsto {e_1} {\textit{fl}:x}}, \alert{\sfpointsto {x} {\textit{fl}:e_2}}, 428 \Sigma}{\Pi',\Sigma'}} 429{\entailment{\eta,\pi,\Pi,\alert{\sflist(\textit{tl}, e_1, e_2)},\Sigma}{\Pi',\Sigma'}} 430\] 431\begin{itemize} 432\item logic can not consider the content of a list 433\item therefore, two cases are sufficient 434\item no induction needed! 435\item similar inference exists for arbitrary trees 436\item however, in general useful for decision procedure 437\end{itemize} 438\end{frame} 439 440\begin{frame} 441\frametitle{\textsf{Append-list}} 442\[\small 443\eqinferstyle 444\inferrule[Append-list] 445{\entailment{\eta,(e_1,e_2),\pi,\alert{\pfunequal{e_1}{e_3}},\Pi,\Sigma}{\Pi',\alert{\sflist(\textit{tl},e_2, e_3)},\Sigma'}} 446{\entailment{\eta,\pi,\alert{\pfunequal{e_1}{e_3}},\Pi,\alert{\sflist(\textit{tl},e_1, 447 e_2)},\Sigma}{\Pi',\alert{\sflist(\textit{tl},e_1, e_3)},\Sigma'}} 448\] 449\begin{itemize} 450\item this inference holds under some complicated side condition 451\item it is preferable to unrolling lists 452\item its correctness proof uses unrolling of lists and simple unrolls and the 453 frame inference 454\end{itemize} 455\end{frame} 456 457 458\begin{frame} 459\frametitle{\textsf{Decision Procedure}} 460\begin{itemize} 461\item these inferences can be easily combined to form a decision procedure for entailments 462\item apply inferences in arbitrary order as long as possible 463\item be careful with \textsf{NIL-NOT-LVAL}, \textsf{Partial}, 464 \textsf{Hypothesis} to avoid looping 465\item iff the entailment could not be reduced to true, it is false 466\item remaining entailments are as simple, that a concrete counterexample can 467 be easily constructed 468\end{itemize} 469 470\end{frame} 471 472\section{HOL embedding} 473\subsection*{} 474 475\begin{frame} 476\frametitle{HOL embedding} 477\begin{itemize} 478\item deep embedding in HOL is straight forward except for trees 479\item trees are introduced considering their maximal depth 480\item equivalence with other recursive definition is formally proofed 481\item inferences are implemented as conversions 482\item the decision procedure is implemented as a conversion 483\end{itemize} 484\end{frame} 485 486\begin{frame} 487\frametitle{HOL embedding II} 488 489\begin{tabular}{|l|r|} 490\hline 491 & \textbf{LOC} \\\hline\hline 492deep embedding and inferences & approx. 10\,000 \\ 493special versions of inferences for conversions & approx. 2\,500 \\ 494conversions and decision procedure & approx. 2\,000 \\\hline 495\end{tabular} 496 497\end{frame} 498 499\section{Example} 500\subsection*{} 501 502\begin{frame} 503\frametitle{example from \texttt{list.sf}} 504\[\small\begin{array}{lr} 505\only<1>{\alert{\pfunequal {x_0} \nil,\pfunequal {x_1} \nil, \pfunequal {x_2} \nil, 506\pfunequal {x_0} {x_3}, \pfunequal {x_0} {x_2}, \pfunequal {x_4} {x_5},}}\\ 507\only<1>{\alert{\pfunequal {x_1} {x_3}, 508\pfunequal {x_1} {x_2}, \pfunequal {x_3} {x_2}}} 509\only<2>{\Pi},\\ 510\sfpointsto {x_2} {\textit{hd}:x_5, \textit{tl}:x_3}, 511\sflist(\textit{tl},x_3,\nil), \sflist(\textit{tl},x_1,x_0), 512\sfpointsto {x_0} {\textit{tl},x_2} & \vdash \\ 513\sflist(\textit{tl},x_1,x_2), \sfpointsto {x_2} {\textit{tl}:x_3}, \sflist(\textit{tl},x_3,\nil) 514\end{array} 515\] 516\end{frame} 517 518\begin{frame} 519\frametitle{example inference application} 520\[\small\begin{array}{llc} 521\Pi,\alert<2>{\sfpointsto {x_2} {\textit{hd}:x_5, \textit{tl}:x_3}},\\ 522\alert<2>{\sflist(\textit{tl},x_3,\nil)}, \sflist(\textit{tl},x_1,x_0), 523\sfpointsto {x_0} {\textit{tl},x_2} & \vdash & \onslide<2->{\textsc{\tiny Frame}} \\ 524\sflist(\textit{tl},x_1,x_2), \alert<2>{\sfpointsto {x_2} {\textit{tl}:x_3}}, 525\alert<2>{\sflist(\textit{tl},x_3,\nil)} & & \pause \alert<2>{\Longleftrightarrow} \\ 526\\ 527 528\alert<2>{x_2},\alert<2>{(x_3,\nil)},\Pi, \alert<3>{\sflist(\textit{tl},x_1,x_0)}, 529\sfpointsto {x_0} {\textit{tl},x_2} & \vdash & \onslide<3->{\text{\textsc{\tiny Append-List}}} \\ 530\alert<3>{\sflist(\textit{tl},x_1,x_2)} & & \pause \alert<3>{\Longleftrightarrow} \\ 531\\ 532 533 534x_2,(x_3,\nil),\alert<3>{(x_1,x_0)},\Pi, 535\alert<4>{\sfpointsto {x_0} {\textit{tl},x_2}} & \vdash & \onslide<4->{\textsc{\tiny Simple-Unroll}} \\ 536\alert<4>{\sflist(\textit{tl},\alert<3>{x_0},x_2)} & & \pause \alert<4>{\Longleftrightarrow} \\ 537\\ 538 539 540x_2,\alert<4>{x_0},(x_3,\nil),(x_1,x_0),\Pi & \vdash & \onslide<5->{\textsc{\tiny Remove-Trivial}} \\ 541\alert<5>{\sflist(\textit{tl},\alert<4>{x_2},x_2)} & & \pause\alert<5>{\Longleftrightarrow} \\ 542\\ 543 544 545x_2,x_0,(x_3,\nil),(x_1,x_0),\Pi & \vdash & \onslide<6->{\textsc{\tiny Axiom}} \\ 546 & & \pause \alert<6>{\Longleftrightarrow} \\ 547 548\top 549\end{array} 550\] 551\end{frame} 552 553\begin{frame}[fragile] 554\frametitle{example HOL} 555\begin{semiverbatim}\scriptsize 556val t = ``LIST_DS_ENTAILS ([],[]) 557 ([pf_unequal (dse_var 0) dse_nil; 558 pf_unequal (dse_var 1) dse_nil; 559 pf_unequal (dse_var 2) dse_nil; 560 pf_unequal (dse_var 0) (dse_var 3); 561 pf_unequal (dse_var 0) (dse_var 2); 562 pf_unequal (dse_var 4) (dse_var 5); 563 pf_unequal (dse_var 1) (dse_var 3); 564 pf_unequal (dse_var 1) (dse_var 2); 565 pf_unequal (dse_var 3) (dse_var 2)], 566 [sf_points_to (dse_var 2) [("hd",dse_var 5); ("tl", dse_var 3)]; 567 sf_ls "tl" (dse_var 3) dse_nil; 568 sf_ls "tl" (dse_var 1) (dse_var 0); 569 sf_points_to (dse_var 0) [("tl", (dse_var 2))]]) 570 571 ([], 572 [sf_ls "tl" (dse_var 1) (dse_var 2); 573 sf_points_to (dse_var 2) [("tl", dse_var 3)]; 574 sf_ls "tl" (dse_var 3) dse_nil])``; 575\end{semiverbatim} 576\end{frame} 577 578\begin{frame}[fragile] 579\frametitle{example HOL II} 580\begin{semiverbatim}\scriptsize 581val thm1 = 582(ds_inference_FRAME___CONV THENC 583 ds_inference_APPEND_LIST___CONV THENC 584 ds_inference_SIMPLE_UNROLL___CONV THENC 585 ds_inference_REMOVE_TRIVIAL___CONV THENC 586 ds_inference_AXIOM___CONV) t; 587 588val thm2 = ds_DECIDE_CONV t; 589\end{semiverbatim} 590\end{frame} 591 592\section{Conclusions and Future Work} 593\subsection*{} 594 595\begin{frame} 596\begin{block}{Conclusions} 597\begin{itemize} 598\item there is a deep embedding of the decidable fragment of separation logic 599 used by \smallfoot 600\item all inferences used by \smallfoot\ have been verified using HOL 601\item a decision procedure for entailments has been implemented 602\end{itemize} 603\end{block} 604 605\begin{block}{Future Work} 606\begin{itemize} 607\item add symbolic execution to build a \smallfoot\ implementation in HOL 608\item extend the logic 609\item try interactive proofs for more complicated fragments of separation logic 610\end{itemize} 611\end{block} 612 613\end{frame} 614 615\end{document} 616 617%%% Local Variables: 618%%% mode: latex 619%%% TeX-master: "presentation" 620%%% End: 621