3 ms·

In the landing page example: > But if we run the model checker, we find that’s not true: Alice could trade an item to herself and, before that process finishes

In the landing page example: > But if we run the model checker, we find that’s not true: Alice could trade an item to herself and, before that process finishes running, resolve a parallel trade giving that same item to Bob. Then the first trade resolves and Alice gets the item back. How does the model checker know that "parallel threads" are even a possibility here? It seems like it's checking what amounts to a leaky abstraction from the actual implementation of this algorithm. In my mind a strictly logical validator would look at the proposed algorithm and say it checks out (since in math-land transactions are atomic). Is this just a feature of the model checker? Can it be turned off/tuned to the expected real-world implementations of the algorithm?

loup-vaillant 8y ago
TLA+ is originally mainly meant to check for concurrency bugs, so the possibility of parallel threads is kind of in its core DNA. The name "process" might also give a hint that parallel threads are indeed possible. I don't know how, but I expect you can indeed model actual transactions.
- hwayne 8y ago
  Depends on what you mean by "actual transaction". Every TLA+ behavior is describable as a series of "next-states", where _usually_ (not always, but _usually_) one action is true. In which case you'd model the transaction by determining the changes that the overall transaction makes and then declaring them all as part of a single action.
gmfawcett 8y ago
It's a feature. When you specify the algorithm, you also specify which actions are atomic, and which aren't.
strangecasts 8y ago
PlusCal uses labels (e.g. "Give:") to designate atomic actions - when you translate it, each labelled section is turned into an atomic action [1]. You can start off with a very simple spec with totally atomic transactions, and gradually make it more granular by introducing more labels, as shown in Wayne's Strange Loop presentation [2] [1] https://learntla.com/concurrency/labels/ https://learntla.com/concurrency/labels/ [2] https://youtu.be/_9B__0S21y8?t=955 https://youtu.be/_9B__0S21y8?t=955 (15:55)
hwayne 8y ago
A general rule-of-thumb in TLA+ is "default is worst-case". If you don't explicitly declare your actions are fair, they'll be unfair. If you don't explicitly encode atomicity into your spec, it's not atomic. Much better to accidentally get a false positive than a false negative.

loup-vaillant 8y ago

TLA+ is originally mainly meant to check for concurrency bugs, so the possibility of parallel threads is kind of in its core DNA. The name "process" might also give a hint that parallel threads are indeed possible. I don't know how, but I expect you can indeed model actual transactions.

hwayne 8y ago
Depends on what you mean by "actual transaction". Every TLA+ behavior is describable as a series of "next-states", where _usually_ (not always, but _usually_) one action is true. In which case you'd model the transaction by determining the changes that the overall transaction makes and then declaring them all as part of a single action.

gmfawcett 8y ago

It's a feature. When you specify the algorithm, you also specify which actions are atomic, and which aren't.

strangecasts 8y ago

PlusCal uses labels (e.g. "Give:") to designate atomic actions - when you translate it, each labelled section is turned into an atomic action [1]. You can start off with a very simple spec with totally atomic transactions, and gradually make it more granular by introducing more labels, as shown in Wayne's Strange Loop presentation [2] [1] https://learntla.com/concurrency/labels/ https://learntla.com/concurrency/labels/ [2] https://youtu.be/_9B__0S21y8?t=955 https://youtu.be/_9B__0S21y8?t=955 (15:55)

hwayne 8y ago

A general rule-of-thumb in TLA+ is "default is worst-case". If you don't explicitly declare your actions are fair, they'll be unfair. If you don't explicitly encode atomicity into your spec, it's not atomic. Much better to accidentally get a false positive than a false negative.