Skip to content

add logical orders to handles

Jaehwang Jung requested to merge jaehwang/handle-logical-order into graphs_multi

The most notable additions are orders_consistent (logical order implies physical view inclusion) and SeenEvents (the handle has seen the output view of events it's aware of) defined in linearizability/spec.v. The structure of client proofs (queue/proof_mp_lin.v, queue/proof_exchange_lin.v) are largely unchanged.

@jaemin.choi Please create a separate MR for event_list_helper lemmas.

Merge request reports