Commits · d9d4c5043b1c3b764dd6fc27396193e718743341 · Iris / gpfsl

30 Sep, 2021 5 commits
- 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
15 Sep, 2021 1 commit
- Restructure exchanger spec a bit · a29597a5
  Hai Dang authored Sep 15, 2021
  
  a29597a5
14 Sep, 2021 3 commits
- Update w.r.t. WP notation · 85f881ff
  Hai Dang authored Sep 14, 2021
  
  85f881ff
- Use weakestpre notation from upstream · a2cdf0ba
  Hai Dang authored Sep 14, 2021
  
  a2cdf0ba
- Add some TODOs · 44649cc2
  Hai Dang authored Sep 14, 2021
  
  44649cc2
13 Sep, 2021 2 commits
- Minor cleanup of Treiber stack graph proof · e3f1b422
  Hai Dang authored Sep 13, 2021
  
  e3f1b422
- Fix graph specs; Add basic graph spec for stack · c439fa48
  Hai Dang authored Sep 13, 2021
  
  c439fa48
12 Sep, 2021 1 commit
- Weaken graph stack spec to fit elim stack · 1adbd987
  Hai Dang authored Sep 12, 2021
  
  1adbd987
09 Sep, 2021 3 commits
- Fix comments in mp exchanger client · c47a5a57
  Hai Dang authored Sep 09, 2021
  
  c47a5a57
- Cleanup and more comments on mp exchanger client · 8af6ad93
  Hai Dang authored Sep 09, 2021
  
  8af6ad93
- More clean up of mp exchange client · 7304cc6c
  Hai Dang authored Sep 09, 2021
  
  7304cc6c