Commits · cb5784886c49e00f194af1953d68df48fff316fc · Iris / gpfsl

01 Oct, 2021 7 commits
- Also remove seqP · cb578488
  Hai Dang authored Oct 01, 2021
  
  cb578488
- Remove seq.v · 1f4d38a1
  Hai Dang authored Oct 01, 2021
  
  1f4d38a1
- Move lattice_cmra · 08cfdf76
  Hai Dang authored Oct 01, 2021
  
  08cfdf76
- Simplify uses of agree gmap in atomics and GPS · e34a6e25
  Hai Dang authored Oct 01, 2021
  
  e34a6e25
- Add a TODO for the history construction · 25447704
  Hai Dang authored Oct 01, 2021
  
  25447704
- Cleanup some list lemmas · b9875441
  Hai Dang authored Oct 01, 2021
  
  b9875441
- Add gset and list GPS protocols · faafa10b
  Hai Dang authored Oct 01, 2021
  
  faafa10b
30 Sep, 2021 8 commits
- Extend stack graph spec: union of local assertions · fab74b31
  Hai Dang authored Sep 30, 2021
  
  fab74b31
- Fix Treiber stack proof · 9d2e4b9f
  Hai Dang authored Sep 30, 2021
  
  9d2e4b9f
- Update Treiber stack spec and proof · 25738bf2
  Hai Dang authored Sep 30, 2021
  
  25738bf2
- Cleanup atomic cmra a bit · d9d4c504
  Hai Dang authored Sep 30, 2021
  
  d9d4c504
- Extend stack graph spec with timeless local assertion · 723f7158
  Hai Dang authored Sep 30, 2021
  
  723f7158
- Fix w.r.t. to_agree change · dcae3994
  Hai Dang authored Sep 30, 2021
  
  dcae3994
- Add more lemmas for graph ghost · e5c8cb98
  Hai Dang authored Sep 30, 2021
  
  e5c8cb98
- Add gmap_inj · f5d61515
  Hai Dang authored Sep 30, 2021
  
  f5d61515
29 Sep, 2021 6 commits
- Strength AtomicSeen rules w.r.t agreement · 45c78092
  Hai Dang authored Sep 29, 2021
  
  45c78092
- A cleanup · b737ac8e
  Hai Dang authored Sep 29, 2021
  
  b737ac8e
- Generalize cmra for atomics · 865c120f
  Hai Dang authored Sep 29, 2021
  
  865c120f
- Revert changes to graph stack spec: StackLocal available earlier at commit view · 50d3e847
  Hai Dang authored Sep 29, 2021
  
  50d3e847
- Fix stack spec to sync on comm view · d2c56796
  Hai Dang authored Sep 29, 2021
  
  d2c56796
- Revert "Weaken view relations of matching pairs for queue/stack" · ab7c1182
  Hai Dang authored Sep 29, 2021
```
This reverts commit ad7f241b.
```
  ab7c1182
28 Sep, 2021 1 commit
- Weaken view relations of matching pairs for queue/stack · ad7f241b
  Hai Dang authored Sep 28, 2021
  
  ad7f241b
27 Sep, 2021 1 commit
- Add consistency lemmas for empty graphs · 7d268b32
  Hai Dang authored Sep 27, 2021
  
  7d268b32
24 Sep, 2021 2 commits
- Fix warning in mp stack client · e30ae5d5
  Hai Dang authored Sep 24, 2021
  
  e30ae5d5
- Move xo_eco to base stack consistency · cf6f46c5
  Hai Dang authored Sep 24, 2021
  
  cf6f46c5
21 Sep, 2021 3 commits
- Revert removal of some defs in exchanger graph spec · 8c0c5d04
  Hai Dang authored Sep 21, 2021
  
  8c0c5d04
- Fix private post conditions for graph specs · 80d9cc73
  Hai Dang authored Sep 21, 2021
  
  80d9cc73
- Revert "Remove private post from atomic wp" · 725fe8af
  Hai Dang authored Sep 21, 2021
```
This reverts commit 9895a2ed.

Because we need post condition after invariants are closed.
```
  725fe8af
19 Sep, 2021 10 commits
- Fix wrong path in _CoqProject · d7b8bf1b
  Hai Dang authored Sep 19, 2021
  
  d7b8bf1b
- Add mp client with stack to _CoqProject · b0705955
  Hai Dang authored Sep 19, 2021
  
  b0705955
- Merge branch 'stack-mp' into 'graphs_multi' · 1c8e2b4b
  Hai Dang authored Sep 19, 2021
```
stack MP client

See merge request iris/gpfsl!21
```
  1c8e2b4b
- Clean up stack graph mp client proof · 848100e3
  Hai Dang authored Sep 19, 2021
  
  848100e3
- stack MP client · 0e467f6f
  William Mansky authored Sep 16, 2021 and Hai Dang committed Sep 19, 2021
  
  0e467f6f
- Minor proof cleanup · aaee3a4a
  Hai Dang authored Sep 19, 2021
  
  aaee3a4a
- Clean up some graph client proofs a bit · 25641b4c
  Hai Dang authored Sep 19, 2021
  
  25641b4c
- Add a TODO · c49dc22c
  Hai Dang authored Sep 19, 2021
  
  c49dc22c
- Add a TODO · d8928490
  Hai Dang authored Sep 19, 2021
  
  d8928490
- Add per elem spec for queue · fc3b61f0
  Hai Dang authored Sep 19, 2021
  
  fc3b61f0
16 Sep, 2021 2 commits
- Improve atomic update mask frame lemma, thanks to David Swasey · a50b60f5
  Hai Dang authored Sep 16, 2021
  
  a50b60f5
- Repackaging some of exchanger spec defs · c9a699b6
  Hai Dang authored Sep 16, 2021
  
  c9a699b6