Commits · master · Simon Friis Vindum / examples

01 May, 2020 1 commit
- Implement new approach to proof of original variant · ce7591fc
  Simon Friis Vindum authored May 01, 2020
  
  ce7591fc
30 Apr, 2020 1 commit
- Refactor refinement proof · e5d87d29
  Simon Friis Vindum authored Apr 30, 2020
  
  e5d87d29
29 Apr, 2020 1 commit
- Add Java stdlib inspired tail shortcut · f84a8254
  Simon Friis Vindum authored Apr 29, 2020
  
  f84a8254
23 Apr, 2020 2 commits
- Use fractional pointers with extensional variable · 3458a611
  Simon Friis Vindum authored Apr 23, 2020
  
  3458a611
- Refactor shared lemmas into common module · d22e9418
  Simon Friis Vindum authored Apr 23, 2020
  
  d22e9418
22 Apr, 2020 1 commit
- Fix the last admits in the refinement proof · 90f2dac1
  Simon Friis Vindum authored Apr 22, 2020
  
  90f2dac1
21 Apr, 2020 16 commits
- Simplify queue refinement proof a bit · 60e4913d
  Simon Friis Vindum authored Apr 20, 2020
  
  60e4913d
- Add proof of alternative MS queue with a few holes · 6c87654d
  Simon Friis Vindum authored Apr 18, 2020
  
  6c87654d
- Refactor specification and proofs · 65994941
  Simon Friis Vindum authored Apr 15, 2020
  
  65994941
- Simplify proofs · a9ce84fb
  Simon Friis Vindum authored Apr 09, 2020
  
  a9ce84fb
- Qed the refinement proof · b25580f8
  Simon Friis Vindum authored Apr 07, 2020
  
  b25580f8
- Dequeue almost done with new approach · 12e687ca
  Simon Friis Vindum authored Apr 06, 2020
  
  12e687ca
- New approach to sentinel invariant · 1b351c46
  Simon Friis Vindum authored Apr 05, 2020
  
  1b351c46
- Add pseudo code for MS queue and cleanup a few things · aa0d4950
  Simon Friis Vindum authored Apr 01, 2020
  
  aa0d4950
- Dequeue proof goes through on empty queue but no longer on non-empty queue · f796a363
  Simon Friis Vindum authored Mar 31, 2020
  
  f796a363
- Proove enqueue · 732cf2e5
  Simon Friis Vindum authored Mar 29, 2020
  
  732cf2e5
- Correct mistake in node invariant and advance enqueue proof · c43c2908
  Simon Friis Vindum authored Mar 28, 2020
  
  c43c2908
- Advance enqueue proof, include node invariant in queue invariant · b9d834bb
  Simon Friis Vindum authored Mar 27, 2020
  
  b9d834bb
- Finish dequeue non-empty case when CAS succeeds · 40a015c2
  Simon Friis Vindum authored Mar 26, 2020
  
  40a015c2
- Advance dequeue proof when queue is non-empty · a802fb7c
  Simon Friis Vindum authored Mar 25, 2020
  
  a802fb7c
- Use fractional points-to predicates, fix nodeInv, and more · 3ddd6bed
  Simon Friis Vindum authored Mar 25, 2020
  
  3ddd6bed
- Add WIP Michael-Scott queue · bed9cc46
  Simon Friis Vindum authored Mar 25, 2020
  
  bed9cc46
18 Apr, 2020 2 commits
- replace gc.v by inv_heap Iris lib · 99f8ad18
  Ralf Jung authored Apr 18, 2020
  
  99f8ad18
- update dependencies · 66c22fad
  Ralf Jung authored Apr 18, 2020
  
  66c22fad
15 Apr, 2020 1 commit
- update dependencies · b7b9be1c
  Ralf Jung authored Apr 15, 2020
  
  b7b9be1c
10 Apr, 2020 1 commit
- Merge branch 'ralf/string-ident' into 'master' · 38c5bcec
  Ralf Jung authored Apr 10, 2020
```
use string-ident plugin a bit

See merge request !32
```
  38c5bcec
08 Apr, 2020 1 commit
- update dependencies · 0a8f1911
  Ralf Jung authored Apr 08, 2020
  
  0a8f1911
07 Apr, 2020 2 commits
- use string-ident plugin a bit · 61034040
  Ralf Jung authored Apr 07, 2020
  
  61034040
- update dependencies · 10d32e09
  Ralf Jung authored Apr 07, 2020
  
  10d32e09
06 Apr, 2020 1 commit
- bump CI to Coq 8.11.1 · 6cd6fd08
  Ralf Jung authored Apr 06, 2020
  
  6cd6fd08
04 Apr, 2020 3 commits
- some missing fixes · 53c8c569
  Ralf Jung authored Apr 04, 2020
  
  53c8c569
- fix for latest Iris · c5f21766
  Ralf Jung authored Apr 04, 2020
  
  c5f21766
- update dependencies · ddf3194b
  Ralf Jung authored Apr 04, 2020
  
  ddf3194b
03 Apr, 2020 1 commit
- Bump Iris. · 7068d035
  Robbert Krebbers authored Apr 03, 2020
  
  7068d035
02 Apr, 2020 4 commits
- order warning whitelist consistently · 8fde0c22
  Ralf Jung authored Apr 02, 2020
  
  8fde0c22
- fix for oFunctor_apply · c13658d5
  Ralf Jung authored Apr 02, 2020
  
  c13658d5
- no longer silence ambiguous coercion paths, and fix other warnings · b07b7deb
  Ralf Jung authored Apr 02, 2020
  
  b07b7deb
- update dependencies · 2ec13e91
  Ralf Jung authored Apr 02, 2020
  
  2ec13e91
18 Mar, 2020 1 commit
- update dependencies · 2897dca2
  Ralf Jung authored Mar 18, 2020
  
  2897dca2
16 Mar, 2020 1 commit
- update dependencies; fix for Iris notation/coercion change · 8f6100ac
  Ralf Jung authored Mar 16, 2020
  
  8f6100ac