Commits · masters/weak_mem · Iris / lambda-rust

Mar 11, 2021
- add GhostCell proof by Joshua Yanovski · 97946ce6
  Ralf Jung authored 4 years ago
  
  97946ce6
- add BrandedVec proof by Joshua Yanovski · 4376ac7f
  Ralf Jung authored 4 years ago
  
  4376ac7f
- make external lifetime context inclusion syntactic, and adjust type system and existing proofs · ac7ba2d6
  Ralf Jung authored 4 years ago
  
  ac7ba2d6
- add derived 'meta' mechanism to lifetime logic: associate a lifetime with metadata (via a gname) · 1da46577
  Ralf Jung authored 4 years ago
  
  1da46577
Feb 12, 2021
- diverging_static can now be checked in the type system · 5b40fd70
  Ralf Jung authored 4 years ago
  
  5b40fd70
Sep 03, 2020
- sync warning settings · 5705e5d7
  Ralf Jung authored 4 years ago
  
  5705e5d7
Sep 02, 2020
- update warning settings, and fix warnings · ceb6ca55
  Ralf Jung authored 4 years ago
  
  ceb6ca55
Apr 02, 2020
- enable coercion path warning · 2e75ac23
  Ralf Jung authored 5 years ago
  
  2e75ac23
Nov 07, 2019
- Ignore more warnings (copied from Iris). · 25c5306a
  Robbert Krebbers authored 5 years ago
  
  25c5306a
- Update Coq flags in _CoqProject. · d5989fe9
  Robbert Krebbers authored 5 years ago
  
  d5989fe9
May 26, 2019
- comment why warnings got disabled · 2337b126
  Ralf Jung authored 6 years ago
  
  2337b126
- comment on disabled warnings · 08b78a76
  Ralf Jung authored 6 years ago
  
  08b78a76
May 12, 2019
- silence annoyingly verbose deprecation warning · f479c17d
  Ralf Jung authored 6 years ago
  
  f479c17d
- silence annoyingly verbose deprecation warning · 3369b5ca
  Ralf Jung authored 6 years ago
  
  3369b5ca
Feb 15, 2019
- bump gpfsl · 31e47d88
  Hai Dang authored 6 years ago
  
  31e47d88
Sep 18, 2018
- ported spawn · 3c8a1ed0
  Hai Dang authored 6 years ago
  
  3c8a1ed0
Sep 04, 2018
- WIP: atomic gps · 76ae5540
  Hai Dang authored 6 years ago
  
  76ae5540
Sep 01, 2018
- Port lock+mutex to combined GPS · 256b1de3
  Hai Dang authored 6 years ago
  
  256b1de3
Aug 20, 2018
- port fake shared uniq ref · 7231d4d7
  Hai Dang authored 6 years ago
  
  7231d4d7
Aug 08, 2018
- also prove faking a shared uniq ref · e6a4bef4
  Ralf Jung authored 6 years ago
  
  e6a4bef4
Jun 30, 2018
- add arc typing to build · 1baf04b4
  Hai Dang authored 6 years ago
  
  1baf04b4
Jun 28, 2018
- WIP: arc typing proof · 5d157208
  Hai Dang authored 6 years ago
  
  5d157208
Jun 24, 2018
- add arc basic specs to build · e403c6f8
  Hai Dang authored 6 years ago
  
  e403c6f8
Jun 09, 2018
- finish rwlock, build with iris's fupd_step_wp branch and gpfsl's step_fupd branch · 2830609b
  Hai Dang authored 7 years ago
  
  2830609b
Jun 06, 2018
- almost finish rwlock, only rwlockreadguard drop code left · dbe8fbd7
  Hai Dang authored 7 years ago
  
  dbe8fbd7
- complete rwlock write code, WIP: rwlock code · f1983fc8
  Hai Dang authored 7 years ago
  
  f1983fc8
Jun 05, 2018
- bump gpfsl and WIP rwlock code · b6760d1c
  Hai Dang authored 7 years ago
  
  b6760d1c
Jun 04, 2018
- WIP: rwlock readguard code · 812d9b21
  Hai Dang authored 7 years ago
  
  812d9b21
- complete rwlock acquire code · 9b69b59d
  Hai Dang authored 7 years ago
  
  9b69b59d
Jun 03, 2018
- WIP: rwlock code · f6252a2b
  Hai Dang authored 7 years ago
  
  f6252a2b
- fix build · 4bb7220e
  Hai Dang authored 7 years ago
  
  4bb7220e
May 31, 2018
- WIP: rwlock code · 2ad690bd
  Hai Dang authored 7 years ago
  
  2ad690bd
- rwlockreadguard type · c915f494
  Hai Dang authored 7 years ago
  
  c915f494
- rwlock typing · de90bc2d
  Hai Dang authored 7 years ago
  
  de90bc2d
May 26, 2018
- complete spawn/join · fed91e19
  Hai Dang authored 7 years ago
  
  fed91e19
- spec for spawn · 3c37666f
  Hai Dang authored 7 years ago
  
  3c37666f
May 24, 2018
- complete mutexguard · 82ec5a40
  Hai Dang authored 7 years ago
  
  82ec5a40
- complete mutex · d9c8590e
  Hai Dang authored 7 years ago
  
  d9c8590e
- bump gpfsl; WIP mutex · cde6200e
  Hai Dang authored 7 years ago
  
  cde6200e
- Update coqproject. · f4dc9fc0
  Jacques-Henri Jourdan authored 7 years ago
  
  f4dc9fc0