Commit f52177bf by Hai Dang

Minor fixes

parent 082d7aa1
 ... ... @@ -58,7 +58,7 @@ Definition enqueue_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)} (enqueue : val) Eo (QueueLocal : QueueLocalT Σ) (QueueInv : QueueInvT Σ) : Prop := ∀ (q: loc) tid γg G1 M (V : view) (v : Z) (Posx: 0 < v), (* PRIVATE PRE *) ⊒V -∗ QueueLocal γg q G1 M -∗ (* (G1,E1) is a snapshot of the graph, locally observed by M *) ⊒V -∗ QueueLocal γg q G1 M -∗ (* G1 is a snapshot of the graph, locally observed by M *) (* PUBLIC PRE *) <<< ∀ G, ▷ QueueInv γg G >>> enqueue [ #q ; #v] @ tid; Eo ... ... @@ -77,7 +77,7 @@ Definition enqueue_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)} come with the Enqueue (acquired by reading the Head pointer). *) ∧ enqId ∉ M ⌝, (* RETURN VALUE AT COMMITTING POINT *) RET #☠, True >>> RET #☠, emp >>> . Definition dequeue_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)} ... ... @@ -110,7 +110,7 @@ Definition dequeue_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)} enqId ∈ M' ∧ deqId ∈ M' ∧ deqId ∉ M ∧ ∃ eV, G.(Es) !! enqId = Some eV ∧ eV.(ge_event) = enq ∧ eV.(ge_lview) ⊆ M') ) ⌝, (* RETURN VALUE AT COMMITTING POINT *) RET #v, True >>> RET #v, emp >>> . ... ... @@ -138,7 +138,7 @@ Definition try_enq_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)} G'.(so) = G.(so) ∧ G'.(com) = G.(com) ∧ enqId ∈ M' ∧ enqId ∉ M ⌝, (* RETURN VALUE AT COMMITTING POINT *) RET #b, True >>> RET #b, emp >>> . Definition try_deq_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)} ... ... @@ -173,7 +173,7 @@ Definition try_deq_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)} enqId ∈ M' ∧ deqId ∈ M' ∧ deqId ∉ M ∧ ∃ eV, G.(Es) !! enqId = Some eV ∧ eV.(ge_event) = enq ∧ eV.(ge_lview) ⊆ M') ) ⌝, (* RETURN VALUE AT COMMITTING POINT *) RET #v, True >>> RET #v, emp >>> . (** Bundling of specs *) ... ...
 ... ... @@ -60,7 +60,7 @@ Definition try_push_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR sevent)} (try_push : val) Eo (StackLocal : StackLocalT Σ) (StackInv : StackInvT Σ) : Prop := ∀ (s: loc) tid γg G1 M (V : view) (v : Z) (Posx: 0 < v), (* PRIVATE PRE *) (* (G1,E1) is a snapshot of the graph, locally observed by M *) (* G1 is a snapshot of the graph, locally observed by M *) ⊒V -∗ StackLocal γg s G1 M -∗ (* PUBLIC PRE *) <<< ∀ G, ▷ StackInv γg s G >>> ... ... @@ -89,7 +89,7 @@ Definition push_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR sevent)} (push : val) Eo (StackLocal : StackLocalT Σ) (StackInv : StackInvT Σ) : Prop := ∀ (s: loc) tid γg G1 M (V : view) (v : Z) (Posx: 0 < v), (* PRIVATE PRE *) (* (G1,E1) is a snapshot of the graph, locally observed by M *) (* G1 is a snapshot of the graph, locally observed by M *) ⊒V -∗ StackLocal γg s G1 M -∗ (* PUBLIC PRE *) <<< ∀ G, ▷ StackInv γg s G >>> ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!