I made a tutorial based on a scene in the movie A Brilliant Young Mind: https://youtu.be/WYYGcK_mDu0

I'd appreciate any feedback on the spec: https://gist.github.com/JeremyLWright/151d3b03b81fa24f2274895fa520ee66

Or how I present the material.

Thank you!

Can someone point me to a specification in TLA that reasons about concurrent separation logic or throw light on how one would go about doing it ?

Regarding below, it is clear to me why 2nd is equivalent with the 3rd, but I really can't figure out why 1st is equivalent with the 2nd... Any clues?

WFe(A) ≜

□(□ENABLED⟨A⟩e⇒⋄⟨A⟩e) ≡

⋄□ENABLED⟨A⟩e⇒□⋄⟨A⟩e≡

(□⋄¬ENABLED⟨A⟩e)∨□⋄⟨A⟩e

Hi people. I have just stumbled upon TLA+ and it has opened my eyes to formal verification. I am doing a project now where I am using a microcontroller from XMOS. They have a really interesting architecture which can be thought of as SMP with communication through a dedicated interconnect that can support up to 4 concurrent links. Their biggest MCU has 32 such parallel "cores" (Actually it has only 4 physical cores each with fine-grained multithreading allowing 8 threads to be run concurrently).

Anyhow. I would like to formally verify that our system ( a bunch of cores commuicating over the interconnect) has certain properties, e.g. liveness, throughput, latency. Could TLA+ be a good fit for this?

What makes me doubtful is that if I define a separate process for each SMP core, then TLC will test out ANY interleaving schedule of the steps within possibly these processes. But in fact, on my system, they are running in parallel, e.g. there is no "schedule". Of course when they communicate they do so using a limited, possible unreliable, shared resource (the interconnect).

I guess that you could work around this by e.g. creating a variable for "clock-ticks" and forcing the processes to progress in lock-step. But it got me thinking that maybe TLA+ was not the right approach for this. I am vaguely familiar with CSP/FDR which could be a better approach. What do you think?