Commits · 43371d2a41e20d8a43721bdc945a09a2f3755349 · Iris / examples

Jun 18, 2019
- prepare for API-triggered builds · 43371d2a
  Ralf Jung authored 5 years ago
  
  43371d2a
Jun 13, 2019
- bump Iris · 2deb5e0d
  Ralf Jung authored 5 years ago
  
  2deb5e0d
- Bump Iris. · 86460eea
  Robbert Krebbers authored 5 years ago
  
  86460eea
Jun 12, 2019
- show that snapshot needs no control at all over the other location · 392a0d4a
  Ralf Jung authored 5 years ago
  
  392a0d4a
- restructure snapshot to not actually have a protocol on the y location · 45ad940f
  Ralf Jung authored 5 years ago
  
  45ad940f
- give readable names to the two possible states of the counter · c67a9a51
  Ralf Jung authored 5 years ago
  
  c67a9a51
- expand comments · 82d08c14
  Ralf Jung authored 5 years ago
  
  82d08c14
- actually we don't need the meta stuff for cinc · b14af24e
  Ralf Jung authored 5 years ago
  
  b14af24e
Jun 11, 2019
- bump Iris; fix for frac_auth notation changes · ae3400d6
  Ralf Jung authored 5 years ago
  
  ae3400d6
- equip remaining specs with the fact that names are countable (just in case) · d21da3ed
  Ralf Jung authored 5 years ago
  
  d21da3ed
- have a dedicated spec file for cinc, and show that we have an instance · e72057ce
  Ralf Jung authored 5 years ago
  
  e72057ce
- cinc: some more small tweaks · 0c530c68
  Ralf Jung authored 5 years ago
  
  0c530c68
- cinc: deduplicate per-update protocol initialization · bd3bc54e
  Ralf Jung authored 5 years ago
  
  bd3bc54e
- simplify conditional counter: get rid of histories; instead of heap metadata for ABA protection · 67ee87b8
  Ralf Jung authored 5 years ago
  
  Also needs a new token and splitting ownership of the "main" protocol location.
  67ee87b8
Jun 10, 2019
- bump Iris, fix for gen_heap supporting heap metadata · 03ad2ac9
  Ralf Jung authored 5 years ago
  
  03ad2ac9
- bump Iris · 4f20e572
  Ralf Jung authored 5 years ago
  
  4f20e572
Jun 06, 2019
- Bump Iris. · 870930c1
  Robbert Krebbers authored 5 years ago
  
  870930c1
Jun 05, 2019
- bump Iris · 0b700e2b
  Ralf Jung authored 5 years ago
  
  0b700e2b
- bump Iris · 6a2e17fa
  Ralf Jung authored 5 years ago
  
  6a2e17fa
- Bump Iris. · 0d9e2d1b
  Robbert Krebbers authored 5 years ago
  
  0d9e2d1b
Jun 04, 2019
- Merge branch 'fix_and_cinc' into 'master' · b3159ec2
  Ralf Jung authored 5 years ago
  
  Fix and conditional increment example See merge request !19
  b3159ec2
- New conditional increment example. · 31b7db5f
  Rodolphe Lepigre authored 5 years ago
  
  Verified
  
  31b7db5f
- Fix atomic snapshot and update to last Iris. · 08108eb8
  Rodolphe Lepigre authored 5 years ago
  
  Verified
  
  08108eb8
- Get rid of `ρ` argument of `spec_ctx`. · fcd5c1de
  Robbert Krebbers authored 5 years ago
  
  fcd5c1de
May 31, 2019
- Merge branch 'fix' into 'master' · d4f41539
  Ralf Jung authored 5 years ago
  
  Some [positive] was sometimes used for [loc], which is now abstract. See merge request !18
  d4f41539
- Some [positive] was sometimes used for [loc], which is now abstract. · 5ec0e1f5
  Rodolphe Lepigre authored 5 years ago
  
  Verified
  
  5ec0e1f5
- bump Iris · 3e2bbf56
  Ralf Jung authored 5 years ago
  
  3e2bbf56
May 28, 2019
- Merge branch 'robbert/barrier_auth' into 'master' · 890575d6
  Robbert Krebbers authored 5 years ago
  
  Shorter barrier proof that uses auth instead of sts. See merge request !16
  890575d6
- Shorter barrier proof that uses auth instead of sts. · 5e4112d3
  Robbert Krebbers authored 5 years ago
  
  5e4112d3
May 26, 2019
- fix comment · 79d26fe9
  Ralf Jung authored 5 years ago
  
  79d26fe9
- remove unnecessary disabled warning · 2b29e580
  Ralf Jung authored 5 years ago
  
  2b29e580
- comment on disabled warnings · 84cd2bac
  Ralf Jung authored 5 years ago
  
  84cd2bac
- bump Iris · 73e9b893
  Ralf Jung authored 5 years ago
  
  73e9b893
May 25, 2019
- bump Iris · 941ee36f
  Ralf Jung authored 5 years ago
  
  941ee36f
- flat combiner: use solve_inG · d8edb4e8
  Ralf Jung authored 5 years ago
  
  d8edb4e8
- logrel: fix for Coq master · 2d6aa0bd
  Ralf Jung authored 5 years ago
  
  2d6aa0bd
- bump Iris · 42d6747d
  Ralf Jung authored 5 years ago
  
  42d6747d
- silence extremely verbose deprecation warning · f615cfe0
  Ralf Jung authored 5 years ago
  
  f615cfe0
- bump Coq base version to 8.9.0 · 837bc704
  Ralf Jung authored 5 years ago
  
  837bc704
- do nightly build against Coq 8.10 branch · 2044cfbe
  Ralf Jung authored 5 years ago
  
  2044cfbe