pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising before class

Browse source
This commit is contained in:
Adam Chlipala 2020-04-28 09:40:40 -04:00
parent 300f78191e
commit 5f735225ef
2 changed files with 13 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
ConcurrentSeparationLogic.v
View file

@ -19,8 +19,8 @@ Set Asymmetric Patterns.
Notation heap := (fmap nat nat). Notation heap := (fmap nat nat).
Notation locks := (set nat). Notation locks := (set nat).
Hint Extern 1 (_ <= _) => linear_arithmetic. Hint Extern 1 (_ <= _) => linear_arithmetic : core.
Hint Extern 1 (@eq nat _ _) => linear_arithmetic. Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core.
Ltac simp := repeat (simplify; subst; propositional; Ltac simp := repeat (simplify; subst; propositional;
try match goal with try match goal with
@ -206,7 +206,7 @@ Module Import S <: SEP.
t. t.
Qed. Qed.
Hint Resolve split_empty_bwd'. Hint Resolve split_empty_bwd' : core.
Theorem extra_lift : forall (P : Prop) p, Theorem extra_lift : forall (P : Prop) p,
P P
@ -488,7 +488,7 @@ Proof.
apply try_me_first_easy. apply try_me_first_easy.
Qed. Qed.
Hint Resolve try_ptsto_first. Hint Resolve try_ptsto_first : core.
(** ** The nonzero shared counter *) (** ** The nonzero shared counter *)
@ -829,7 +829,7 @@ Qed.
* book PDF for a sketch of the important technical devices and lemmas in this * book PDF for a sketch of the important technical devices and lemmas in this
* proof. *) * proof. *)
Hint Resolve himp_refl. Hint Resolve himp_refl : core.
Lemma invert_Return : forall linvs {result : Set} (r : result) P Q, Lemma invert_Return : forall linvs {result : Set} (r : result) P Q,
hoare_triple linvs P (Return r) Q hoare_triple linvs P (Return r) Q
@ -844,7 +844,7 @@ Proof.
rewrite IHhoare_triple; eauto. rewrite IHhoare_triple; eauto.
Qed. Qed.
Hint Constructors hoare_triple. Hint Constructors hoare_triple : core.
Lemma invert_Bind : forall linvs {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q, Lemma invert_Bind : forall linvs {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q,
hoare_triple linvs P (Bind c1 c2) Q hoare_triple linvs P (Bind c1 c2) Q

8
frap_book.tex
View file

@ -4745,7 +4745,7 @@ Here's the object language we adopt, which should be old hat by now, just mixing
$$\begin{array}{rrcl} $$\begin{array}{rrcl}
\textrm{Commands} & c &::=& \mt{Fail} \mid \mt{Return} \; v \mid x \leftarrow c; c \mid \mt{Loop} \; i \; f \\ \textrm{Commands} & c &::=& \mt{Fail} \mid \mt{Return} \; v \mid x \leftarrow c; c \mid \mt{Loop} \; i \; f \\
&&& \mid \mt{Read} \; a \mid \mt{Write} \; a \; v \mid \mt{Lock} \; a \mid \mt{Unlock} \; a \mid c || c &&& \mid \mt{Read} \; a \mid \mt{Write} \; a \; v \mid \mt{Alloc} \; n \mid \mt{Free} \; a \; n \mid \mt{Lock} \; a \mid \mt{Unlock} \; a \mid c || c
\end{array}$$ \end{array}$$
$$\infer{\smallstep{(h, l, x \leftarrow c_1; c_2(x))}{(h', l', x \leftarrow c'_1; c_2(x))}}{ $$\infer{\smallstep{(h, l, x \leftarrow c_1; c_2(x))}{(h', l', x \leftarrow c'_1; c_2(x))}}{
@ -4762,6 +4762,12 @@ $$\infer{\smallstep{(h, l, \mt{Read} \; a)}{(h, l, \mt{Return} \; v)}}{
\msel{h}{a} = v \msel{h}{a} = v
}$$ }$$
$$\infer{\smallstep{(h, \mt{Alloc} \; n)}{(\mupd{h}{a}{0^n}, \mt{Return} \; a)}}{
\dom{h} \cap [a, a+n) = \emptyset
}
\quad \infer{\smallstep{(h, \mt{Free} \; a \; n)}{(h - [a, a+n), \mt{Return} \; ())}}{
}$$
$$\infer{\smallstep{(h, l, \mt{Lock} \; a)}{(h, l \cup \{a\}, \mt{Return} \; ())}}{ $$\infer{\smallstep{(h, l, \mt{Lock} \; a)}{(h, l \cup \{a\}, \mt{Return} \; ())}}{
a \notin l a \notin l
} }