[w3c/IndexedDB] Add TLA+ spec for core concurrency of spec (PR #484)

This PR comes out of the blue, but I think it could be useful. 

It adds a TLA+ spec for what I think is the core concurrent part of the spec: the transaction and connection lifecycle. 

As background: I am involved in the efforts at Servo to implement the latest spec, and I found how the above is specified to be quite ambiguous at first. Once you've internalized the spec and thought about it, I think it all makes sense, but the benefit of expressing this in TLA+ is that it abstracts away everything else and provides you with an unambiguous description of the concurrent part that a machine can check. 

Note sure how to integrate this in the actual spec; maybe via a note and a link to the file in the repo?

For your consideration.
You can view, comment on, or merge this pull request online at:

  https://github.com/w3c/IndexedDB/pull/484

-- Commit Summary --

  * add tla+ spec for transaction lifecycle
  * second pass on spec
  * third pass: add invariant for request only processed when can start
  * remove tabs
  * remove redundant pre-conditions; add docs
  * simply start and finish of open
  * fix deadlock in open flow following simplification
  * track request processing with just a boolean
  * fix transaction ordering
  * add rejecting of open
  * revert version change on abort
  * add invariant for overlapping started transactions
  * group invariants together
  * bound connection queue
  * fix autocommit
  * fix docs

-- File Changes --

    M .gitignore (3)
    A transaction_lifecycle.cfg (16)
    A transaction_lifecycle.tla (423)

-- Patch Links --

https://github.com/w3c/IndexedDB/pull/484.patch
https://github.com/w3c/IndexedDB/pull/484.diff

-- 
Reply to this email directly or view it on GitHub:
https://github.com/w3c/IndexedDB/pull/484
You are receiving this because you are subscribed to this thread.

Message ID: <w3c/IndexedDB/pull/484@github.com>