Commit 08670a05 authored by Zhen Zhang's avatar Zhen Zhang

Add docs folder back

parent e3c94895
\setmonofont{Source Code Pro}
\newif\ifslow\slowfalse %\slowtrue
\usepackage[top=1in, bottom=1in, left=1.25in, right=1.25in]{geometry}
\title{\bfseries iris-atomic}
\author{Zhen Zhang}
\text{synced}(R, f', f) \eqdef
\All P, Q, x.
&\hoare{ R * P(x)}{f(x)}{ v.\,R * Q(x,v) } \ra \\
&\hoare{ P(x)}{f'(x)}{ v.\,Q(x,v) }
\text{is\_syncer}(R, s) \eqdef
\All f. \wpre{s(f)}{ f'.\, \text{synced}(R, f', f)} \]
mk\_syncer\_spec (mk\_syncer) :=
\All R.
\hoare{R}{mk\_syncer()}{ s.\,\always (is\_syncer(R, s)} \]
Logically atomic triple:
\lahoare{g.\, \alpha(g)}{e}{v.\, \beta(g, v)}[E_i][E_o] \eqdef
\All P, Q.
&P \vs[Eo][Ei] \Exists g, \alpha(g) * (\alpha(g) \vsW[Ei][Eo] P \land \All v. \beta(g, v) \vsW[Ei][Eo] Q(g, v)) \wand \\
&\hoare{P}{e}{v.\, \Exists g. Q(g, v)}
mk_sync :=
λ: <>,
let l := newlock() in
λ: f x,
acquire l;
let ret := f x in
release l;
Specialized logically atomic triple:
\[ \lahoare{g.\, \ownGhost{\gname}{g^{1/2}} * \always \alpha(g)}
{v.\, \Exists g'. \ownGhost{\gname}{g'^{1/2}} * \beta(x, g, g', v)}[E_i][E_o]\]
sync(mk_syncer) :=
λ: f_seq l,
let s := mk_syncer() in
s (f_seq l).
\[seq\_spec(f, \phi, \alpha, \beta, E) \eqdef
\All l.
\pure &\All x, \Phi, g.\\
&\phi (l, g) * \always \alpha(x) *\\
&(\All v, g'. \phi(l, g') \wand \beta(x, g, g', v) \wand \pvs[E][E] \Phi(v))\\
&\proves \wpre{f'(x)}[E]{ \Phi }
&\text{atomic\_spec}(mk\_syncer, f\_seq, l, \phi, \alpha, \beta, E_i) \eqdef\\
&\All g_0.
seq\_spec(f\_seq, \phi, \alpha, \beta, \top) \ra
mk\_syncer\_spec(mk\_syncer) \ra\\
&\phi(l, g_0)
\proves \wpre{sync(mk\_syncer, f\_seq, l)}{ f.\,
\Exists \gname. \ownGhost{\gname}{g_0^{1/2}} *
\All x. \always \lahoare{g.\, \ownGhost{\gname}{g^{1/2}} * \always \alpha(g)}{f(x)}
{v.\, \Exists g'. \ownGhost{\gname}{g'^{1/2}} * \beta(x, g, g', v)}[E_i][\top]}
\end{aligned} \]
\[ (\Exists g. \phi(l, g') * \ownGhost{\gname}{g^{1/2}} * P x \]
push s x :=
let hd := !s in
let s' := ref SOME (x, hd) in
if CAS s hd s'
then ()
else push s x.
pop s :=
let hd := !s in
match !hd with
| SOME (x, hd') =>
if: CAS s hd hd'
then SOME x
else pop s
iter hd f :=
match !hd with
| NONE => ()
| SOME (x, hd') => f x ; iter hd' f
Logiall atomic spec (version 1):
\[ \lahoare{xs.\, stack(s, xs)}{push(s, x)}{stack(s, x::xs)}[heapN][\top]\]
\[ \lahoare{xs.\, stack(s, xs)}{pop(s)}{v. \begin{split} (&\Exists x, xs'. v = SOME(x) * stack(s, xs')) \lor\\
(&v = NONE * xs = \emptyset * stack(s, \emptyset)) \end{split}}[heapN][\top]\]
Logiall atomic spec (version 2):
\[ \lahoare{hd, xs.\, s \mapsto hd * list(hd, xs)}{push(s, x)}{\Exists hd'. s \mapsto hd' * hd' \mapsto SOME(x, hd) * list(hd, xs)}[heapN][\top]\]
\[ \lahoare{hd, xs.\, s \mapsto hd * list(hd, xs)}{pop(s)}{v.
(&\Exists x, xs', hd'. v = SOME(x) * hd \mapsto SOME(x, hd') * s \mapsto hd' * list(hd', xs')) \lor\\
(&v = NONE * xs = \emptyset * hd \mapsto NONE)
A crappy but working spec:
\[f\_spec (\gname, xs, s, f, Rf, RI) \eqdef
\All x.
\hoare{x \in xs * \knowInv\iname{\Exists xs. stack'(\gname, xs, s) * RI} * Rf}{f(x)}{ v.\, v = () }.\]
iter\_spec(\gname, s, Rf, RI) \eqdef
&\All xs, hd, f.\\
&f\_spec(xs, s, f', Rf, RI) \ra\\
&\hoare{\knowInv\iname{\Exists xs. stack'(xs, s) * RI} * list'(\gname, hd, xs) * Rf}{iter(hd, f)}{ v.\, v = () * Rf}
\[push\_spec (\gname, s, x, RI) \eqdef
\hoare{R(x) * \knowInv\iname{\Exists xs. stack'(xs, s) * RI}}{push(s, x)}{v.\, v = () * (\Exists hd. ev(\gname, hd, x))}\]
doOp :=
λ: p,
match !p with
| InjL (f, x) => p <- InjR (f x)
| InjR _ => ()
try_srv :=
λ: lk s,
if try_acquire lk
then let hd := !s in
iter hd doOp;
release lk
else ().
loop p s lk :=
match !p with
| InjL _ =>
try_srv lk s;
loop p s lk
| InjR r => r
install :=
λ: f x s,
let p := ref (InjL (f, x)) in
push s p;
mk_flat :=
λ: <>,
let lk := newlock() in
let s := new_stack() in
λ: f x,
let p := install f x s in
let r := loop p s lk in
\[p \mapsto \injR(-)\]
\[p \mapsto \texttt{injL}(f, x)\]
\[p \mapsto \injR(y)\]
\[\circ_i, \bullet_i, \dia_i, \bdia, \dia_i \circ_i, \dia_i \bullet_i, \bdia \bullet_i\]
&\Exists y. &&p \fmapsto[1/2] \injR(-) * \dia_i * \circ_i\\
\lor &\Exists f, x, P, Q. &&p \fmapsto[1/2] \injL(f, x) * \ownGhost{\gname}{x^{1/2}} *
P(x) * (\hoare{R * P(x)}{f(x)}{v.\,R * Q(x, v)}) * \gamma \mapstoprop Q(x) * \dia_i * \bullet_i\\
\lor &\Exists x. &&p \fmapsto[1/2] \injL(-, x) * \ownGhost{\gname}{x^{1/4}} * \bdia * \bullet_i\\
\lor &\Exists x, y. &&p \fmapsto[1/2] \injR(y) * \ownGhost{\gname}{x^{1/2}} * \gamma \mapstoprop Q(x) * Q(x, y) * \dia_i * \bullet_i
\[\alpha = \alpha_a * \alpha_o, \alpha = \alpha_a' * \alpha_o\]
\[\alpha = \alpha_o * \alpha_a, \alpha_a' * \alpha_o = \beta\]
\[\alpha = \alpha_a * \alpha_o, \alpha = \alpha_a' * \alpha_o\]
This diff is collapsed.
This diff is collapsed.
% Locallabel
% Copyright (C) 2001, 2002, 2003 Didier Rmy
% Author : Didier Remy
% Version : 1.1.1
% Bug Reports : to author
% Web Site :
% Locallabel is free software; you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation; either version 2, or (at your option)
% any later version.
% Locallabel is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% GNU General Public License for more details
% (
% File locallabel.sty (LaTeX macros)
%% Identification
[2001/23/02 v0.92 Locallabel]
%% Preliminary declarations
%% Options
%% More declarations
%% We use two counters: The global counter is incremented at each reset.
%% Its value is the ``group'' of a local.
%% The local counter is the last numeric value of a bound label in the
%% current group. The value of a label #1 is globally set to
%% \csname llb@\the\c@llb@global-#1\endcsname
%% The global command \csname llb@\the\c@llb@global-#1*\endcsname is
%% use to ensure that a label is only bound once. Usually a label is
%% bound and declared at the same time with \llabel. It may also be bound in
%% advance, with \lbind, for instance so as to control the numbering.
%% Then, another \llabel must be used to declare it in the text.
%% If no \lbind has been used before, the \llabel calls \lbind implicitlt.
\newcommand \llb@find [1]
{\expandafter \ifx \csname llb@\the\c@llb@global-#1\endcsname \relax
\message {*** Local label #1 undefined in this context}%
\edef \llb@current {#1??}%
\edef \llb@current {\csname llb@\the\c@llb@global-#1\endcsname}%
\newcommand \llb@make [1]
{\expandafter \ifx \csname llb@\the\c@llb@global-#1\endcsname \relax
\stepcounter{llb@local}\relax \expandafter
\xdef \csname llb@\the\c@llb@global-#1\endcsname {\the\c@llb@local}%
\edef \llb@current {\the\c@llb@local}%
\expandafter \ifx \csname llb@\the\c@llb@global-#1*\endcsname \relax
\message {*** Local label #1 already defined in this countext!}%
\edef \llb@current {\csname llb@\the\c@llb@global-#1\endcsname ??}%
\expandafter \global \expandafter \let
\csname llb@\the\c@llb@global-#1*\endcsname \relax
\edef \llb@current {\csname llb@\the\c@llb@global-#1\endcsname}
%%% Redefine those macros to change typsetting
\newcommand \thelocallabel {\the \c@llb@local}
\newcommand \LlabelTypeset [1] {(\textrm {\bfseries #1})}
\newcommand \LrefTypeset [1] {(\textrm {#1)}}
\newcommand \glabel [1]{\LlabelTypeset{\softtarget {#1}{#1}}}
\newcommand \gref [1]{\LrefTypeset{\softlink {#1}{#1}}}
%%% To reset all local labels---which just increment a global prefix.
\newcommand \locallabelreset[1][0]%
{\stepcounter {llb@global}\setcounter {llb@local}{#1}}
%%% Make a new local label, typeset it, and bind to the given name
\def \llb@relax {\relax}
\newcommand {\llabel}[2][\relax]%
\def \@test {#1}\ifx \@test\llb@relax\else
\edef \@currentlabel {\the\c@llb@local}%
\def \@test {#1}\ifx \@test\empty \def \@test{#2}\fi
\LlabelTypeset {\softtarget{llb@\the\c@llb@global-#2}{\llb@current}}}
%%% Retreive the local label of given name and type set it.
\newcommand \lref [1]
{\llb@find {#1}%
\LrefTypeset {\softlink {llb@\the\c@llb@global-#1}{\llb@current}}}
%%% Make a new local label and bind it to the given name but do not typeset
%%% it. Typesetting may then be done with \llabel non locally. Useful to
%%% control the order of numberring.
\newcommand \lbind [1]
{\llb@make {#1}%
\expandafter \global \expandafter
\let \csname llb@\the\c@llb@global-#1*\endcsname \empty}
\AtBeginDocument {%
\@ifundefined{softlink}{\let \softlink \@secondoftwo}{}%
\@ifundefined{softtarget}{\let \softtarget \@secondoftwo}{}%
\RequirePackage{\basedir locallabel}
\RequirePackage{Tabbing} % Avoid the standard tabbing environment. Its \< conflicts with the semantic package.
%% Biimplication inference rules
% \biimp above below
% The double lines obtained by the simpler
% "\mprset{fraction={===}}" overlap the conclusion (e.g., the
% mask E_M in an atomic triple).
%% inferH is infer with hyperlinked names.
% \savelabel lab text: Arrange for \ref{lab} to print text and to link to the current spot.
% Think @currentlabel : text ref.
\edef\@currentlabel{#2}% Save text
\phantomsection% Correct hyper reference link
\label{#1}% Print text and store name↦text.
% \textlabel label text: Print and label text.
% \rulenamestyle visible
\newcommand*{\rulenamestyle}[1]{{\TirNameStyle{#1}}} % From mathpartir.sty.
% \ruleref [discharged] lab
% \rulename label
% \inferhref name lab premise conclusion
% \infernH name premise conclusion, if name a valid label.
% The sanity checks in \lbind and \llabel
% don't work properly in amsmath environments
% which perhaps lay out their contents more
% than once. Use \lbind in such cases.
% Sigh.
\newcommand\UNIND{\unind \\}
% Attribution:
%When \left\{ … \right\} looks ugly, remember Dave says you want \bracket.
\NewDocumentCommand{\RES}{s m O{}}{%
\NewDocumentCommand{\ARES}{m O{}}{%
Vars: ${\color{ctxcolor}\displaystyle{#1}}$}
Context: ${\color{ctxcolor}\displaystyle{#1}}$}
Goal: ${\displaystyle{#1}}$}
Suff: ${\displaystyle{#1}}$}
Have: ${\displaystyle{#1}}$}
% A version of \qedhere that accounts for tabbing.
% The starred version lacks leading and trailing vertical space.
{\partopsep=\z@skip \topsep=\z@skip% avoid initial space
\parskip\z@skip% avoid trailing space
\usepackage{\basedir mathpartir}
\usepackage{\basedir pftools}
\usepackage{\basedir iris}
\usepackage{xcolor} % for print version
\SetSymbolFont{stmry}{bold}{U}{stmry}{m}{n} % this fixes warnings when \boldsymbol is used with stmaryrd included
\extrarowheight=\jot % else, arrays are scrunched compared to, say, aligned
% Array {rMcMl} modifies array {rcl}, putting mathrel-style spacing
% around the centered column. (We used this, for example, in laying
% out some of Iris' axioms. Generally, aligned is simpler but aligned
% does not work in mathpar because \\ inherits mathpar's 2em vskip.)
% The capital M stands for THICKMuskip. The smaller medmuskip would be
% right for mathbin-style spacing.
linktocpage=true, pdfstartview=FitV,
breaklinks=true, pageanchor=true, pdfpagemode=UseOutlines,
plainpages=false, bookmarksnumbered, bookmarksopen=true, bookmarksopenlevel=3,
hypertexnames=true, pdfhighlight=/O,
\newcommand{\TODO}{\vskip 4pt {\color{red}\bf TODO}}
\newcommand{\ie}{\emph{i.e.,} }
\newcommand{\eg}{\emph{e.g.,} }
\newcommand{\aaron}[1]{{\color{red}\textbf{AT: #1}}}
\newcommand{\derek}[1]{{\color{red}\textbf{DD: #1}}}
\newcommand{\lars}[1]{{\color{red}\textbf{LB: #1}}}
\newcommand{\kasper}[1]{{\color{red}\textbf{KS: #1}}}
\newcommand{\ralf}[1]{{\color{red}\textbf{RJ: #1}}}
\newcommand{\dave}[1]{{\color{red}\textbf{PDS: #1}}}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment