Commit ce0dc131 authored by Hai Dang's avatar Hai Dang
Browse files

Add some comments

parent edd29130
...@@ -259,7 +259,7 @@ Definition queue_empty_unmatched_enq_strong G : Prop := ...@@ -259,7 +259,7 @@ Definition queue_empty_unmatched_enq_strong G : Prop :=
See more weakenings below. See more weakenings below.
On the other hand, we can also strengthen it further by changing the On the other hand, we can also strengthen it further by changing the
conclusion from (d1,d2) ∈ xo (d1,d2) ∈ eco. *) conclusion from [(d1,d2) ∈ xo] to [(d1,d2) ∈ eco]. *)
Definition queue_FIFO_strong G : Prop := Definition queue_FIFO_strong G : Prop :=
e1 v1 eV1 e2 d2, e1 v1 eV1 e2 d2,
G.(Es) !! e1 = Some eV1 eV1.(ge_event) = Enq v1 G.(Es) !! e1 = Some eV1 eV1.(ge_event) = Enq v1
...@@ -282,7 +282,8 @@ Definition queue_FIFO G : Prop := ...@@ -282,7 +282,8 @@ Definition queue_FIFO G : Prop :=
. .
(* Alternatively, if e2 as an enqueue that has been dequeued but also observed (* Alternatively, if e2 as an enqueue that has been dequeued but also observed
an enqueue e1, then e1 must also have been dequeued. *) an enqueue e1, then e1 must also have been dequeued.
This encodes the Yacovet's condition [com^-1; lhb; com; lhb is irreflexive]. *)
Definition queue_FIFO_weak G := Definition queue_FIFO_weak G :=
e1 d1 dV1 e2 d2 eV2, e1 d1 dV1 e2 d2 eV2,
(e1, d1) G.(com) (e2, d2) G.(com) (e1, d1) G.(com) (e2, d2) G.(com)
......
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