On Wednesday, 13 July 2016 13:22:56 UTC+1, Steve Loughran wrote:
I'm looking for some example specifications of an eventually consistent object store, such as amazon S3.
In the absence of any such spec, I've sat down to start writing my own, and appear to have got stuck due to my lack of understanding of the TLA+ syntax and/or fundamental misunderstandings of the concepts therein. Some help would be appreciated.
1. Defining a function now() which returns a timestamp.
I've done something ugly which fails to include the fact that the timestamp can/should be considered monotonically increasing from some external
source.
CONSTANT now(_)
ASSUME \A t \in Nat: now(t) \in Timestamp
Why the meaningless argument? To distinguish now(0) from "now", which is too like an unchanging constant for my liking, and because now() is illegal.
What should I be doing here?
2. What's the best way to specify postconditions of an operation?
Example: after a delete I want to declare the fact "the path is no longer in the store"
doDelete(path, result) ==
LET
validArgs == path \in Paths
exists == has_entry(store, path)
IN
\/ /\ ~validArgs
/\ result' = BadRequest
/\ UNCHANGED store
\/ /\ validArgs
/\ ~exists
/\ result' = NotFound
/\ UNCHANGED store
\/ /\ validArgs
/\ exists
/\ result' = Success
/\ store' = [p \in (DOMAIN store \ path) |-> store[p]]
/\ ~has_entry(store', path) \* HERE
Now, that's somewhat superfluous given definition of has_entry;
has_entry(s, p) == p \in DOMAIN s
the definition of what store' becomes declares that path isn't in the domain, but by doing it this way I'm spelling out what test. Except if I do it where I have, I'm essentially creating a new outcome, aren't I?
The alternative would be some invariant, though as well as showing up my confusion about predicates vs set refinement, I also have to consider that problem which it only holds if nothing else does a PUT operation between the delete and check.
DeleteInvariant == \A p in Paths: doDelete(p, Success) ==> ~has_entry(store', p)
I don't want to go there yet.
3. Invariants of consistency across operations. How to declare that the metadata from the doGet and the doHead operations are consistent.
GetAndHeadConsistent ==
\A path \in DOMAIN store, sysMd \in SystemMetadata, data \in Data :
doGet(path, Success, data, sysMd) ==> doHead(path, Success, sysMd)
Again, people may think this is obvious, but OpenStack swift can return different object lengths in its doList from its doHead operation. Calling it out provides a clear declaration of an invariant people should write tests for.
I know these will all sound trivial to people that actually understand the details of TLA+ but I'm only getting there, first with a simple definition of a consistent object store API, from which I can then extrapolate to one with eventual consistency, where things like that delete invariant downgrades to "holds after some bounded time period"
-Steve