From 27dfd62d3666aaa6b4c290a3b3d8b5750689b3f5 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 8 Mar 2016 17:49:29 +0100 Subject: [PATCH] docs: safety adequacy --- docs/logic.tex | 13 ++++++++++++- program_logic/adequacy.v | 9 ++++++--- 2 files changed, 18 insertions(+), 4 deletions(-) diff --git a/docs/logic.tex b/docs/logic.tex index 88ec1bbbf..5f358f8d7 100644 --- a/docs/logic.tex +++ b/docs/logic.tex @@ -604,7 +604,7 @@ Here we define $\wpre{\expr'}[\mask]{\Ret\var.\prop} \eqdef \TRUE$ if \expr' = \subsection{Adequacy} -The adequacy statement reads as follows: +The adequacy statement concerning functional correctness reads as follows: \begin{align*} &\All \mask, \expr, \val, \pred, \state, \melt, \state', \tpool'. \\&(\All n. \melt \in \mval_n) \Ra @@ -615,6 +615,17 @@ The adequacy statement reads as follows: \end{align*} where\pred\$ is a \emph{meta-level} predicate over values, \ie it can mention neither resources nor invariants. +Furthermore, the following adequacy statement shows that our weakest preconditions imply that the execution never gets \emph{stuck}: Every expression in the thread pool either is a value, or can reduce further. +\begin{align*} + &\All \mask, \expr, \state, \melt, \state', \tpool'. + \\&(\All n. \melt \in \mval_n) \Ra + \\&( \ownPhys\state * \ownGGhost\melt \proves \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra + \\&\cfg{\state}{[\expr]} \step^\ast + \cfg{\state'}{\tpool'} \Ra + \\&\All\expr'\in\tpool'. \toval(\expr) \neq \bot \lor \red(\expr, \state') +\end{align*} +Notice that this is stronger than saying that the thread pool can reduce; we actually assert that \emph{every} non-finished thread can take a step. + % RJ: If we want this section back, we should port it to primitive view shifts and prove it in Coq. % \subsection{Unsound rules} diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v index 94e2d5e8d..55090ec66 100644 --- a/program_logic/adequacy.v +++ b/program_logic/adequacy.v @@ -112,18 +112,20 @@ Lemma wp_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2 : ✓ m → (ownP σ1 ★ ownG m) ⊑ #> e1 @ E {{ Φ }} → rtc step ([e1], σ1) (t2, σ2) → - e2 ∈ t2 → to_val e2 = None → reducible e2 σ2. + e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2). Proof. - intros Hv ? Hs [i ?]%elem_of_list_lookup He. + intros Hv ? Hs [i ?]%elem_of_list_lookup. destruct (wp_adequacy_own Φ e1 t2 σ1 m σ2) as (rs2&Φs&?&?); auto. { by rewrite -(wp_mask_weaken E ⊤). } destruct (Forall3_lookup_l (λ e Φ r, wp ⊤ e Φ 2 r) t2 (Φ :: Φs) rs2 i e2) as (Φ'&r2&?&?&Hwp); auto. + case He:(to_val e2)=>[v2|]; first by eauto. right. destruct (wp_step_inv ⊤ ∅ Φ' e2 1 2 σ2 r2 (big_op (delete i rs2))); rewrite ?right_id_L ?big_op_delete; auto. by rewrite -wp_eq. Qed. +(* Connect this up to the threadpool-semantics. *) Theorem wp_adequacy_safe E Φ e1 t2 σ1 m σ2 : ✓ m → (ownP σ1 ★ ownG m) ⊑ #> e1 @ E {{ Φ }} → @@ -133,8 +135,9 @@ Proof. intros. destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|]. apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2). - destruct (wp_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2) as (e3&σ3&ef&?); + destruct (wp_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2) as [?|(e3&σ3&ef&?)]; rewrite ?eq_None_not_Some; auto. + { exfalso. eauto. } destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto. right; exists (t2' ++ e3 :: t2'' ++ option_list ef), σ3; econstructor; eauto. Qed. -- GitLab