[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Re: Any examples of a specification of an S3-like object store API?

On 25 July 2016 at 21:20, Andrew Helwer <andrew...@xxxxxxxxx> wrote:
Hi Steve, all good questions.

1. Defining now()

Monotonically-increasing variables make model-checking difficult, because absent restrictions this means the system has an infinite number of possible states and so the model checker will never halt. My advice here is to think carefully about whether a monotonically-increasing global clock is really required for you to achieve the desired semantics. If you absolutely need the global clock, define it thus:

VARIABLE GlobalClock

TypeInvariant == GlobalClock \in Nat

Init == GlobalClock = 0

Tick == GlobalClock' = GlobalClock + 1

Model-checking this is difficult. You'll have to define Nat to be a finite set like 1 .. 100, which means there exist behaviors which probably don't conform to the real world system - like an uninterrupted series of Tick relations until you hit GlobalClock = 100, after which other actions take place. You can mitigate this by not allowing Tick if other actions are enabled, but really this whole approach is messy and you're better off without a monotonically-increasing global clock. Why do you need one?

I really want set a wall time when objects are created. So it's purely a state thing. I suppose I could do something like Apache Spark's clock code, which has >1 implementation of the clock: the wall clock and the test clock.


2. Specifying postconditions

It's best to view primed variable "assignments" and postconditions as one and the same. This is tricky to understand, but when you have an action like this:

ExampleAction ==
/\ x \in {0, 1}
/\ x' = 1 - x

you aren't saying "if x is 0 or 1, then assign 1 - x to x after this action executes". You're saying "the ExampleAction formula is true of a step in a behavior if in the first state x is either 0 or 1, and in the second state x' = 1 - x". This isn't pedantry; moving from the state machine paradigm to the behavior paradigm is critical for understanding the temporal logic component of TLA+. The purpose of a spec is to define a set of correct system behaviors, where a behavior is a sequence of states and a state is an assignment of values to variables. So when you see this:

Init == x = 0

Spec == Init /\ [][ExampleAction]_<<x>>

You understand that spec defines a subset of all behaviors such that Init is true in the first state, and for all steps either the ExampleAction boolean formula is true or it is a stuttering step.

I suspect that I've been too used to other specification systems, ones where things are explicitly split into precond and postcond tests. If instead I'm looking more at the state changes during correct operation, then, I can just mix things up in the /\ statements.


How does this all relate back to your question? Simply, a postcondition of the type you've given is perfectly fine. You can use primed variables in whatever logical statements and checks you want and it will not create a new outcome. What adding conjuncts can do is remove outcomes. For example, if we have the following:

ExampleAction ==
/\ x \in {0, 1}
/\ x' = 1 - x
/\ x' \in {2, 3, 4}

Here we have the "postcondition" check that x' is in the set {2, 3, 4}. It's impossible for ExampleAction to be true of any step, since the conjuncts are clearly contradictory and can never all be true. Tying this back to your example, we have these conjuncts:

/\ store' = [p \in (DOMAIN store \ path) |-> store[p]]
/\ ~has_entry(store', path)  \* HERE

If the first conjunct is true (which will probably always be the case) and the second conjunct (your postcondition) is not, TLC will simply not take this step. Personally I would use the first conjunct as the postcondition in and of itself.

I agree, it is superfluous, except I like to spell out clearly those assertions that are good for testing.

What I think I will try and do is look more at sequences of actions, so that a doPut followed immediately by doGet will return the item that was put. That's is the kind observable state that tests like.


A minor stylistic note: rather than modifying the domain of your store variable, consider mapping undefined paths to a placeholder null value instead.

Noted, except that I do like to use that (DOMAIN store) elsewhere to define the set of paths which have data behind them. I think my life would get more complicated
3. Invariants

I'm not sure I understand this question. Could you specify what doGet and doHead do, and what it means for them to be consistent?

they're essentially the HTTP HEAD/GET calls. HEAD returns whether there's something at a path, and if so: metadata, including length of the file.

GET returns the same metadata and the contents too. For valid implementations: the metadata returned by GET and HEAD must be the same; the data coming back with a GET is that which was most recently submitted with a PUT (absent any intermediate DELETE).

There's also the internal consistency requirements of the Get operation: the data returned in the response is the same length as the length declared in the metadata. Obvious, yes, but evidence implies it doesn't always hold: https://issues.apache.org/jira/browse/HADOOP-11202

And again, any list operation should return the length of all the objects in the object store, keeping them consistent with the actual numbers returned.

These are all the kind of things which filesystems do, so fundamental that everyone tends to take them for granted: ls, stat and cat are consistent in their reporting of data. It turns out that the further you get from your posix-compatible local FS, the less you can rely on these things. What I'm trying to do here is write them down for the implementors of clients of the object store to make sure they've implemented, as well as tell users of the APIs what they can expect.