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