Questions About TLC: Parallelism Efficiency, Caching Behavior, and Java Overloading for State-Dependent Operators

[Quentin DELAMEA]

Hello everyone,

I am currently working on a TLA+ specification that is challenging to model-check with TLC for two main reasons:

- The state space is very large.

- The evaluation of properties (especially invariants) is computationally expensive.

To optimize my workflow, I would appreciate insights or references regarding the following questions about TLC:

1. Parallelism in TLC:

   How does TLC handle parallelism, and how effective is it to use many cores? For instance, would running TLC with ~100 cores be beneficial, or are there diminishing returns due to synchronization overhead or other limitations?

2. Caching in TLC:

   When and how does TLC cache information during model checking? Specifically:

   - Does TLC cache results for constant operators only?

   - Does it require that a (constant or non-constant) operator be called repeatedly with the exact same inputs to leverage caching?

3. Java Overloading for State-Dependent Operators:

   I am aware that constant operators can be overloaded with Java code. However, is it possible to overload state-dependent operators or properties (e.g., invariants) by:

   - Passing state variables as parameters to the operator, or

   - Directly accessing state variables from within the Java code?

If any of these topics have been discussed before, I’d be grateful for pointers to relevant threads or documentation. Otherwise, I’d love to hear your experiences or suggestions!

Thank you in advance for your time and help.

Quentin

[Shane Miller]

See my post today. One of the things I mention is that TLA like all major model checkers does not verify LTL in a MT or distributed manner. 

Now, spin (see again post for refs and links) has something along these lines but it's not currently used much. Although I started with it and like almost everything about it, I ran into a fairness issue tla didn't have. (Thanks, tla! Spin needed a bug fix and i didnt bother after that. Otherwise its performance is great. It compiles to C for fast runs.)

In my work on the RPC example I ran into excessive verification times a bunch. I reduced it by

- keeping process count to a bare minimum. This is darn important. 

- eliminate procedures where possible sticking to macros and definitions if using pluscal

- I also found it useful to permit some slight duplication in code between processes (say when a client and server almost do the same thing differing only by passed arguments) so I could change the specification such that client stuff depends on client stuff only by process.

- my rpc example found 71MM distinct states in 2.5hrs. An hour or two is fine. But I had to use Amazon's mi8xlarge instance with at least 128gb of ram and swap. That's probably nothing in the big scheme of things, but certainly not somethibg my macpro could handle.

- periodically stronger assumptions can help

- be realistic: you may not depending on how much time you want to wait be able to test all features in the same model if too many states are made.

If anybody is knows a proven MT or distributed checker ... let me know! I guess here is where theorem oriented formal models might do better ... but I'm getting over my head there.

--
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/4a01fb5c-48bf-4d4d-8fa1-cedf01489283n%40googlegroups.com.