Skip to content
Snippets Groups Projects

prove spsc example with queue graph spec

Merged prove spsc example with queue graph spec
jaehwang/spsc into graphs_multi
1 unresolved thread
Merged Jaehwang Jung requested to merge jaehwang/spsc into graphs_multi
1 unresolved thread

Merge request reports

Merged by Hai DangHai Dang 3 years ago (Oct 26, 2021 8:51am UTC)

Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
theories/examples/queue/proof_producer_consumer.v 0 → 100644
93 | EmpDeqs_intro
94 (EMPS :
95 ∀ i x (XI : xs !! i = Some x),
96 ∃ xV, G.(Es) !! x = Some xV ∧ xV.(ge_event) = EmpDeq)
97 .
98
99 Local Hint Constructors Produced Consumed EmpDeqs : core.
100
101 (* [vl]: values that will be produced *)
102 Definition PCInv q γg γe γd γx vl : vProp := ∃ G es ds xs,
103 Q.(QueueInv) γg q G ∗
104 Events γe (1/2) es ∗ (* enqueues ordered by po *)
105 Events γd (1/2) ds ∗ (* dequeues ordered by po *)
106 Events γx (1/2) xs ∗ (* empty deqeueus ordered by po *)
107
108 ⌜ seq 0 (length G.(Es)) ≡ₚ es ++ ds ++ xs ∧
  • Hai Dang
    Hai Dang @haidang
    Owner

    Would it be any easier to use the hybrid spec here? Does the hybrid spec have a strong relation like this between the events and the abstract state/list of values?

  • Hai Dang changed this line in version 2 of the diff

    changed this line in version 2 of the diff

  • Jaehwang Jung
    Jaehwang Jung @jaehwang.jung
    Author Developer

    We could have an invariant like es = ds ++ current queue which implies matching, but I think the graph part won't be useful because this example doesn't care about the full consistency of empty dequeues.

  • Hai Dang
    Hai Dang @haidang
    Owner

    I think the graph part is useful in the sense that it already tracks the history for you. Using only an abstract state spec you'd need more ghost state to track that history. This particular example needs both the abstract state and the history and their relation, that's why I thought the hybrid spec would be the most useful. Of course if the hybrid spec is not strong enough yet, we don't have to do it right now.

  • Please register or sign in to reply
  • Hai Dang
  • Hai Dang added 1 commit

    added 1 commit

    Compare with previous version

  • Hai Dang
  • Hai Dang mentioned in commit e41906eb

    mentioned in commit e41906eb

  • Hai Dang merged

    merged

    • Please register or sign in to reply