fixes for atomics and ghost state; resolves #769, resolves #770

Author: mansky1

atomics/SC_atomics.v

@@ -15,10 +15,16 @@ Context `{!VSTGS OK_ty Σ}.
 
 Class atomic_int_impl (atomic_int : type) := { atomic_int_at : share -> val -> val -> mpred;
   atomic_int_at__ : forall sh v p, atomic_int_at sh v p ⊢ atomic_int_at sh Vundef p;
-  atomic_int_conflict : forall sh v v' p, sepalg.nonidentity sh -> atomic_int_at sh v p ∗ atomic_int_at sh v' p ⊢ False }.
+  atomic_int_conflict : forall sh v v' p, sepalg.nonidentity sh -> atomic_int_at sh v p ∗ atomic_int_at sh v' p ⊢ False;
+  atomic_int_isptr : forall sh v p, atomic_int_at sh v p ⊢ ⌜isptr p⌝;
+  atomic_int_timeless sh v p :: Timeless (atomic_int_at sh v p)
+ }.
 
 Class atomic_ptr_impl := { atomic_ptr : type; atomic_ptr_at : share -> val -> val -> mpred;
-  atomic_ptr_conflict : forall sh v v' p, sepalg.nonidentity sh -> atomic_ptr_at sh v p ∗ atomic_ptr_at sh v' p ⊢ False }.
+  atomic_ptr_conflict : forall sh v v' p, sepalg.nonidentity sh -> atomic_ptr_at sh v p ∗ atomic_ptr_at sh v' p ⊢ False;
+  atomic_ptr_isptr : forall sh v p, atomic_ptr_at sh v p ⊢ ⌜isptr p⌝;
+  atomic_ptr_timeless sh v p :: Timeless (atomic_ptr_at sh v p)
+ }.
 
 Context {CS : compspecs} `{AI : atomic_int_impl} {AP : atomic_ptr_impl}.
 

atomics/general_atomics.v

@@ -855,7 +855,7 @@ Ltac start_function1 ::=
               |- _ => idtac
             | s:=?spec':_ |- _ => check_canonical_funspec spec'
             end; change (semax_body V G F s); subst s)
-   end; unfold NDmk_funspec;
+   end;
    (let gv := fresh "gv" in
     match goal with
     | |- semax_body _ _ _ (_, mk_funspec _ _ _ _ ?Pre _) =>
@@ -871,8 +871,15 @@ Ltac start_function1 ::=
                                | (a, b) => _
                                end => intros Espec [a b]
            | λne i, _ => intros Espec i
-           end; simpl fn_body; simpl fn_params; simpl fn_return
-    end;
+           end
+    | |- semax_body _ _ _ (pair _ (NDmk_funspec _ _ _ ?Pre _)) =>
+          split3; [check_parameter_types' | check_return_type | ];
+           match Pre with
+           | (convertPre _ _ (fun i => _)) =>  intros Espec (*DependedTypeList*) i
+           | (fun x => match _ with (a,b) => _ end) => intros Espec (*DependedTypeList*) [a b]
+           | (fun i => _) => intros Espec (*DependedTypeList*) i (* this seems to be named "a" no matter what *)
+           end
+    end; simpl fn_body; simpl fn_params; simpl fn_return;
      cbv[dtfr dependent_type_functor_rec constOF idOF prodOF discrete_funOF ofe_morOF
         sigTOF listOF oFunctor_car ofe_car] in *; cbv[ofe_mor_car];
      rewrite_old_main_pre; rewrite ?argsassert_of_at ?assert_of_at;

atomics/verif_lock.v

@@ -9,12 +9,6 @@ Section mpred.
 
 Context `{!VSTGS OK_ty Σ, !cinvG Σ, atom_impl : !atomic_int_impl (Tstruct _atom_int noattr)}.
 
-(* add these to atomic_int_impl? *)
-Axiom atomic_int_isptr : forall sh v p, atomic_int_at sh v p ⊢ ⌜isptr p⌝.
-#[local] Hint Resolve atomic_int_isptr : saturate_local.
-Axiom atomic_int_timeless : forall sh v p, Timeless (atomic_int_at sh v p).
-#[export] Existing Instance atomic_int_timeless.
-
 #[global] Opaque atomic_int_at.
 
 Section PROOFS.

atomics/verif_lock_atomic.v

@@ -91,7 +91,7 @@ Section PROOFS.
   Proof.
     start_function.
     Intros v.
-    assert_PROP (is_pointer_or_null a) by entailer.
+    assert_PROP (is_pointer_or_null p) by entailer.
     forward_call.
     - Exists v. cancel.
     - entailer!.

lib/proof/spec_SC_atomics.v

@@ -17,8 +17,8 @@ Notation vint z := (Vint (Int.repr z)).
    atomic_int_at__ : forall sh v p, atomic_int_at sh v p ⊢ atomic_int_at sh Vundef p;
    atomic_int_conflict : forall sh v v' p, sepalg.nonidentity sh -> atomic_int_at sh v p ∗ atomic_int_at sh v' p ⊢ False%I;
    atomic_int_isptr : forall sh v p, atomic_int_at sh v p ⊢ ⌜isptr p⌝;
-   atomic_int_timeless : forall sh v p, Timeless (atomic_int_at sh v p);
-   atomic_ptr : type := Tstruct _atom_ptr noattr; 
+   atomic_int_timeless sh v p :: Timeless (atomic_int_at sh v p);
+   atomic_ptr : type := Tstruct _atom_ptr noattr;
    atomic_ptr_at : share -> val -> val -> mpred;
   atomic_ptr_conflict : forall sh v v' p, sepalg.nonidentity sh -> atomic_ptr_at sh v p ∗ atomic_ptr_at sh v' p ⊢ False%I
 }.

lib/proof/verif_locks.v

@@ -17,7 +17,7 @@ Definition Vprog : varspecs. mk_varspecs prog. Defined.
 
 Section mpred.
 
-Context `{!VSTGS OK_ty Σ, !cinvG Σ, atom_impl : !atomic_int_impl (Tstruct _atom_int noattr)}.
+Context `{!VSTGS OK_ty Σ, !cinvG Σ(*, atom_impl : !atomic_int_impl (Tstruct _atom_int noattr)*)}.
 
 
 #[export] Program Instance M : lockAPD := {
@@ -98,8 +98,6 @@ Definition Gprog := lockImports ++ LockASI.
       { eapply semax_pre, semax_ff; go_lower; done. }
   Qed.
 
-Opaque inv_for_lock.
-
   Lemma body_release: semax_body Vprog Gprog f_release release_spec.
   Proof.
   (* the following line should not be necessary;
@@ -112,7 +110,6 @@ Opaque inv_for_lock.
     - destruct h as ((p, i), g); simpl; Intros.
       subst Frame; instantiate (1 := []); simpl; cancel.
       iIntros "(HR & #I & ? & P & HQ)".
- (* the next line fails for some reason 
       iInv i as "((% & >p & ?) & Hown)" "Hclose".
       destruct b.
       + iExists Ews; rewrite (bi.pure_True (writable_share _)) //.
@@ -127,7 +124,6 @@ Opaque inv_for_lock.
         rewrite bi.affinely_elim; iNext; iApply ("HR" with "[$]").
     - entailer!.
   Qed.
-*) Admitted.
 
   Lemma body_acquire: semax_body Vprog Gprog f_acquire acquire_spec.
   Proof.
@@ -151,7 +147,7 @@ Opaque inv_for_lock.
     - unfold lock_inv; destruct h as ((p, i), g); Intros.
       subst Frame; instantiate (1 := []); simpl fold_right_sepcon; cancel.
       iIntros "(#I & ?)".
- (* the next line fails for some reason 
+      rewrite {1}/inv_for_lock /=.
       iInv "I" as "((% & >? & ?) & ?)" "Hclose".
       iExists Ews, (Val.of_bool b); rewrite (bi.pure_True (writable_share _)) //.
       iFrame.
@@ -165,8 +161,9 @@ Opaque inv_for_lock.
     - Intros r. if_tac; forward_if; try discriminate; try contradiction.
       + forward. simpl lock_inv; entailer!.
       + forward. simpl lock_inv; entailer!.
-  Qed. *)
-  Admitted.
+  Qed.
+
+Opaque inv_for_lock.
 
 #[global] Opaque M.
 

lib/test/verif_incr.v

@@ -3,7 +3,9 @@ Require Import VST.floyd.VSU.
 Require Import VST.concurrency.conclib.
 From VSTlib Require Import spec_locks spec_threads spec_malloc.
 Require VSTlib.verif_locks.
+Require Import iris_ora.algebra.ext_order.
 Require Import iris_ora.logic.cancelable_invariants.
+Require Import iris.algebra.lib.excl_auth.
 Require Import VSTlibtest.incr.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
@@ -12,11 +14,12 @@ Definition Vprog : varspecs. mk_varspecs prog. Defined.
 #[export] Existing Instance verif_locks.M.
 #[export] Existing Instance verif_malloc.M.
 
+Canonical Structure excl_authR A := inclR (excl_authR A).
 
 Section mpred.
-Context `{VSTGS1: !VSTGS unit Σ, 
-          cinvG1: !cinvG Σ, 
-          inG1: !inG Σ (excl_authR natO), 
+Context `{VSTGS1: !VSTGS unit Σ,
+          cinvG1: !cinvG Σ,
+          inG1: !inG Σ (excl_authR natO),
           aii1: !atomic_int_impl (Tstruct _atom_int noattr)}.
 
 Definition spawn_spec := DECLARE _spawn spawn_spec.
@@ -216,7 +219,6 @@ Proof.
   ghost_alloc (fun g => own g (●E O ⋅ ◯E O : excl_authR natO)).
   { apply excl_auth_valid. }
   Intro g2.
-  sep_apply (library.create_mem_mgr gv).
   forward_call (gv, fun _ : lock_handle => cptr_lock_inv g1 g2 ctr).
   Intros lock.
   forward.
@@ -253,11 +255,13 @@ Proof.
   { lock_props.
     rewrite -{2}Qp.half_half -frac_op -lock_inv_share_join.
     subst ctr; cancel. }
-  forward. 
+  forward.
   unfold_data_at (data_at_ _ _ _). simpl.
   cancel.
-  admit.
- Admitted.
+  unfold cptr_lock_inv; Intros z x y; cancel.
+  rewrite -(field_at_share_join _ _ Ews); [|eauto]; cancel.
+  by iIntros "(_ & _ & _ & _)".
+ Qed.
 
 (*
 

lib/test/verif_incr_main.v

@@ -23,7 +23,7 @@ Definition AB_VSU :=
 Require VSTlib.verif_locks.
 Definition ABC_VSU:=
   ltac:(linkVSUs AB_VSU 
-         (verif_locks.LockVSU (atom_impl := aii1))).
+         (verif_locks.LockVSU)).
 
 Ltac SC_tac ::=
  match goal with |- SC_test ?ids _ _ =>
@@ -42,13 +42,13 @@ Ltac SC_tac ::=
           end.
 
 Definition core_VSU :=
-  ltac:(linkVSUs (IncrVSU (aii1:=aii1)) ABC_VSU).
+  ltac:(linkVSUs IncrVSU ABC_VSU).
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition main_QPprog := ltac:(QPprog prog).
 Definition whole_prog := ltac:(QPlink_progs main_QPprog (VSU_prog core_VSU)).
 Definition Vprog: varspecs := QPvarspecs whole_prog.
-Definition Main_imports := filter (matchImportExport main_QPprog) (VSU_Exports core_VSU). 
+Definition Main_imports := filter (matchImportExport main_QPprog) (VSU_Exports core_VSU).
 
 Definition main_spec :=
  DECLARE _main

progs/incr.c

@@ -1,7 +1,7 @@
 #include "../concurrency/threads.h"
 //#include <stdio.h>
 
-typedef struct counter { unsigned ctr; lock_t *lock; } counter;
+typedef struct counter { unsigned ctr; lock_t lock; } counter;
 counter c;
 
 void incr() {
@@ -21,16 +21,16 @@ int thread_func(void *thread_lock) {
   //Increment the counter
   incr();
   //Yield: 'ready to join'.
-  release((lock_t *)thread_lock);
+  release((lock_t)thread_lock);
   return 0;
 }
 
-int main(void)
+int compute2(void)
 {
   c.ctr = 0;
   c.lock = makelock();
   release(c.lock);
-  lock_t *thread_lock = makelock();
+  lock_t thread_lock = makelock();
   /* Spawn */
   spawn((void *)&thread_func, (void *)thread_lock);
 
@@ -49,3 +49,7 @@ int main(void)
 
   return t;
 }
+
+int main(void) {
+ return compute2();
+}