[tlaplus] Seeking insights on how to translate TLA+ spec into real code

[olilent2ctw@xxxxxxxxx]

Hi all,

Actions of TLA+ specs change global states atomically and a behavior in TLA+ is represented by a series of atomically executed actions. Since in real system implementation, different actions may or may not be allowed executed concurrently, it can be tricky to translate TLA+ spec to real code implementation. Let's take the write-through cache spec in Chapter 5 of Book "Specifying Systems" for example.

DoWr(p1) action and DoRd(p2) action will both access the same cache line of processor p2 if p1 is writing to an address which exists in p2's cache. This requires each cache entry to have a mutual exclusion mechanism. 

In addition, for DoWr(p) action, updating cache and updating memQ'probably should be execute atomically (hold the same mutex), while updating cache and updating buf/ctrl may not need to be an atomic step.

This example is small and simple. However, in real system, reasoning about the what locks are needed and when is it safe to release locks can still be challenging. 

Does anyone have any advice or principles for engineer on how to make aggressive and yet safe optimization to low level implementation details when translating TLA+ spec to code?

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.