[tlaplus] Seeking advice about principles of translating TLA+ spec to real code

[Oliver Yang <olilent2ctw@xxxxxxxxx>]

Hi All,

Actions of TLA+ spec are executed atomically. A legal behavior specified by a TLA+ spec consists of a sequence of atomic actions. When translating TLA+ spec to real code, we still need to figure out how to provide the atomicity. Let's take Write-Through Cache in Chapter 5 of Book "Specifying Systems" as an example.

Action DoRd(p1) and Action DoWr(p2) are concurrent operations. They may touch the same cache line of processor p2 if p1 is writing the same cache'd address as p2 is reading from. This means we may need a mutex for each cache line.

In addition, DoWr(p) action requires updating cache and updating memQ to be an atomic step but it doesn't necessarily require updating cache and updating buf/ctrl to be an atomic step.

Figuring out optimal locking/mutual exclusion strategy (when converting spec to code) can still be challenge and error-prone when implementing large concurrent system. It's very easy for engineers to diverge implementation from specification in the process of designing locking strategy

Here are my questions:
(1) IMO, locking strategy is one important aspect of designing concurrent program which TLA+ seems not cover. Is this a right understanding of TLA+ spec?
(2) If it indeed requires figuring out optimal locking strategy (which TLA+ doesn't capture), then does anyone have figured out a set of good principles/disciplines to do that? or We have to develop an ad-hoc locking strategy every time we try to convert TLA+ specs to implementations?

Thanks,

Oliver

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.