Tools enhancements in "Smart Casual Verification of the Confidential Consortium Framework"

[A. Jesse Jiryu Davis]

Hello, I'm reading "Smart Casual Verification of the Confidential Consortium Framework". Markus is a co-author. It's great! The authors succeeded where I had failed and they clearly describe how they did it.

The paper mentions new features in the TLA+ tools:

1. "we manually weighted failure actions to reduce the likelihood of them being chosen"
2. "we implemented depth-first search (DFS) in TLC"
3. "TLC had already been enhanced to support trace validation"
4. In the TLA+ debugger, "we implemented a new unsatisfied breakpoint that activates for each state in T that is found to be unreachable"
5. "T can be visualized as a graph that not only includes all unreachable states but also references the subformula responsible for the state being unreachable"

The paper summarizes this effort as "enhancing the TLC model checker to support trace validation, which involved implementing support for action composition, DFS, improved debugging support, and visualizing the state graph." So I think the enhancements are in both TLC and the VS Code TLA+ debugger.

Question: Am I right that the paper mentions 6 new features, and where can I learn more about them?

Thanks, I know I'm asking for a lot of info.

[Andrew Helwer]

Good list! I had only heard about 3 and 5.

For now unfortunately the answer for where you can learn more about them is "nowhere outside of reading PRs", although Markus does post some demo videos on the TLA+ youtube channel: https://www.youtube.com/@TLAplusFoundation/videos

I think the best way to document these features is to write a bunch of how-to docs on docs.tlapl.us. Using the schema of documentation being split into tutorials, how-to guides, explanation, and reference (from here), I think docs.tlapl.us is a great place to put how-to-guides and conceptual explanations. We are pretty well covered for TLA+ tutorials with Hillel's learntla.com and Leslie's various courses & books, and I think wikis probably aren't a good place for reference documentation, but how-to-guides and conceptual explanations seem like the perfect fit for the docs.tlapl.us wiki. Of course I'm not married to it and we could do something like readthedocs.io instead.

As for who should do the work of writing all the how-to guides, it seems like a good target for foundation funding. After I finish my current project of transitioning TLAPM to use SANY I might be up for it. I do enjoy technical writing. But it's a lot to write and I would be happy to share the load!

Andrew Helwer

--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/2443fd1a-1c35-419a-95b8-72de361f28bdn%40googlegroups.com.

[Finn Hackett]

I was actually surprised to see (4) in this list - somehow I missed that when reading around, looking up video tutorials, etc. It also may be that the button is right there and I didn't realize how to trigger the behavior... (tl;dr yes docs good)

Is there a PR I can look up (for the vscode plugin I assume)? I ended up building something in the same vein, but using a special TLC VIEW directive instead. Curious to see how the debugger version behaves.

Note: I tried the obvious search on Github and got nothing, so I'm resorting to "does anyone remember what / when".

Best,

-Finn

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUWpccsGr9zcyJFiDKJn8GkNQ1rRFvEKoHhJROh1-xOLLg%40mail.gmail.com.

[Markus Kuppe]

A screencast demonstrating the feature is linked from the commit that introduced unsatisfied breakpoints [1]. Additionally, breakpoints now generally support TLA+ breakpoint expressions [2]. Looking ahead, a forthcoming journal version of "Validating Traces of Distributed Programs Against TLA+ Specifications" [3] dedicates additional space to debugging trace validation.

On the technical side, the TLA+ Debugger integrates with TLC’s interpreter, intercepting execution when all variables are defined and a subsequent subformula of the next-state relation Next causes the Next to evaluate to false. For example, in the context of trace validation, the unsatisfied breakpoint will fire if x = 1 and x' = 3 after reading the (current) value from the log/trace file.

----- MODULE Spec -----
VARIABLE x

SomeSubAction ==
/\ x \in Nat
/\ x’ = x + 1

Next ==
\/ SomeSubAction

=====

---- MODULE Trace ——
EXTENDS Spec

TraceNext ==
/\ x’ = ReadValueFromTheLog
/\ SomeSubAction

=====


Relatedly, the newer `constrained` sub-command of TLC’s Dot state-graph “dumper" will cause it to also dump and annotate states that are excluded from the model due to State or Action Constraints.

Markus

[1] https://github.com/tlaplus/tlaplus/commit/f849bf1b8f85960c0c0ca2cae1034a1feeb20b52
[2] https://github.com/tlaplus/tlaplus/pull/1099
[3] https://arxiv.org/abs/2404.16075
[4] https://github.com/tlaplus/tlaplus/commit/24479f74c8a02fbe2f83981ca6210e2f7fa7799f

[Markus Kuppe]

All technical work related to the paper is publicly documented in the CCF and TLA+ GitHub repositories. Good entry points are:

https://github.com/microsoft/CCF/issues?q=label%3A%22tla%22
https://github.com/microsoft/CCF/issues/5057

Below is a non-exhaustive list of more specific pointers:

- "we manually weighted failure actions to reduce the likelihood of them being chosen"

* https://github.com/microsoft/CCF/issues/6537
* https://github.com/microsoft/CCF/pull/6562
* https://github.com/microsoft/CCF/blob/main/tla/consensus/SIMccfraft.tla
* https://github.com/microsoft/CCF/blob/main/tla/consensus/SIMCoverageccfraft.tla
* https://github.com/tlaplus/tlaplus/commit/05d755591382ce1a574142b004e918074807c23f

* Related: RL/QL work stream started with https://github.com/tlaplus/tlaplus/commit/6dfec66b288f5c57296be8630fab9cea0200b2d4


- "we implemented depth-first search (DFS) in TLC”

* https://github.com/tlaplus/tlaplus/pull/867
* https://github.com/tlaplus/tlaplus/commit/62625342a01b96c2839c575b49dce1b8489fae94


- "we implemented a new unsatisfied breakpoint that activates for each state in T that is found to be unreachable”

* https://groups.google.com/g/tlaplus/c/wuJbBRqZdTQ/m/v6mCu99_AQAJ


- "T can be visualized as a graph that not only includes all unreachable states but also references the subformula responsible for the state being unreachable"

* https://github.com/microsoft/CCF/pull/5989#issuecomment-1928816893
* https://github.com/tlaplus/tlaplus/commit/24479f74c8a02fbe2f83981ca6210e2f7fa7799f
* https://github.com/tlaplus/tlaplus/commit/312518885c0f4688fceb1b30d27c2aed61a6628f


- Action composition

* https://github.com/tlaplus/tlaplus/pull/805



I'm also happy to answer specific questions at the next TLA+ Community call on June 3rd.

Markus

[A. Jesse Jiryu Davis]

Terrific, thanks so much Markus.

--
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+u...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/0A74A7BB-29C0-41F6-BD73-E56F4F7F23E8%40lemmster.de.