Commit a3a70c30 authored by Ralf Jung's avatar Ralf Jung

complete writing down the invariant of the barrier protocol

parent 7c8f9427
From algebra Require Export upred_big_op.
From program_logic Require Export sts saved_prop.
From heap_lang Require Export derived heap wp_tactics notation.
......@@ -102,10 +103,11 @@ Section proof.
Notation iProp := (iPropG heap_lang Σ).
Definition waiting (P : iProp) (I : gset gname) : iProp :=
( Q : gmap gname iProp, True)%I.
( Q : gmap gname iProp, (P - Π★{map Q} (λ _ Q, Q))
Π★{map Q} (λ i Q, saved_prop_own SpI i Q))%I.
Definition ress (I : gset gname) : iProp :=
(True)%I.
(Π★{set I} (λ i, Q, saved_prop_own SpI i Q Q))%I.
Definition barrier_inv (l : loc) (P : iProp) (s : stateT) : iProp :=
match s with
......
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