1. 07 Nov, 2016 2 commits
    • Ralf Jung's avatar
      889f7c78
    • Ralf Jung's avatar
      Merge branch 'uncurried-specs' into 'master' · 8d5768cb
      Ralf Jung authored
      Simpler syncer specs
      
      This simplifies the syncer specs.
      The sequential syncer only is slightly improved, by changing
      ```
        Definition synced R (f' f: val) :=
          (□ ∀ P Q (x: val), ({{ R ★ P x }} f x {{ v, R ★ Q x v }}) →
                             ({{ P x }} f' x {{ v, Q x v }}))%I.
      ```
      such that `P`, `Q` don't factor in a dependency on `x` any more. Since all three are quantified at the same time, the two specs are equivalent -- and the one where `P` is not a predicate and `Q` is exactly the postcondition is arguably simpler:
      ```
        Definition synced R (f f': val) :=
          (□ ∀ P Q (x: val), ({{ R ★ P }} f x {{ v, R ★ Q v }}) →
                             ({{ P }} f' x {{ Q }}))%I.
      ```
      
      For the atomic spec, the changes are deeper. The currying on some location `l` is entirely removed. `is_atomic_syncer` better mirrors `is_syncer` from the sequential version. And finally, we use "original" atomic triples and not some modified version thereof (so `atomic_triple_base` is killed).
      
      TODO: Fix `atomic_pcas.v`, it relied on the location currying done by `atomic_sync.v`. However, I don't entirely grok that file. @zhangz could you give that a look?
      
      See merge request !1
      8d5768cb
  2. 02 Nov, 2016 4 commits
  3. 01 Nov, 2016 3 commits
  4. 25 Oct, 2016 1 commit
  5. 24 Oct, 2016 4 commits
  6. 20 Oct, 2016 4 commits
  7. 19 Oct, 2016 5 commits
  8. 17 Oct, 2016 2 commits
  9. 13 Oct, 2016 4 commits
  10. 12 Oct, 2016 1 commit
  11. 11 Oct, 2016 10 commits