# Re: Any examples of a specification of an S3-like object store API?

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
/\ 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.