Dedalus versus TLA+

[ovidiu...@gmail.com]

Hello,

Can you help with a dedalus versus tla+ comparison and any comment on the following: (from this paper https://dl.acm.org/doi/pdf/10.1145/3639257):

Section 6.3

We chose the Dedalus temporal logic language because it was both amenable to our optimization goals and we knew we could compile it to high-performance machine code via Hydroflow. Temporal logics have also been used for verification of protocols—most notably Lamport’s TLA+ language [44], which has been adopted in applied settings [50]. TLA+ did not suit our needs for a number of reasons. Most notably, efficient code generation is not a goal of the TLA+ toolchain. Second, an optimizer needs lightweight checks for properties (FDs, monotonicity) in the inner loop of optimization; TLA+ is ill-suited to that case. Finally, TLA+ was designed as a finite model checker: it provides evidence of correctness (up to 𝑘 steps of execution) but no proofs. There are efforts to build symbolic checkers for TLA+ [42], but again these do not seem well-suited to our lightweight setting.

Many thanks.

Ovidiu

[Leslie Lamport]

Dear Ovidiu,

 

I don’t have time to read about Dedalus.  However, there are three significant errors in your email.

 

1.  TLA+ was designed as a finite model checker

 

TLA+ is a language not a model checker.  That language was designed without any thought of there being a model checker for it.

 

2. it provides evidence of correctness (up to 𝑘 steps of execution)

 

There are two model checkers for TLA+.  Apalache is a symbolic model checker that checks executions of up to k steps. (It was first used a few years ago.)  TLC is an explicit-state model checker with no such limitation.  (It was first used around 2000.)  It can check a finite-state model of a spec.

 

3.  but no proofs.

 

The TLAPS proof checker for TLA+ was written around 2007.

 

Cheers,

 

Leslie Lamport

 

From: tla...@googlegroups.com <tla...@googlegroups.com> On Behalf Of ovidiu...@gmail.com
Sent: Sunday, June 16, 2024 23:55
To: tlaplus <tla...@googlegroups.com>
Subject: [tlaplus] Dedalus versus TLA+

 

You don't often get email from ovidiu...@gmail.com. Learn why this is important

--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/1166e069-9bd7-4ff3-906d-3962512e6d7dn%40googlegroups.com.

[Ovidiu Marcu]

Dear Leslie,

Thank you for your feedback. Looks like their comparison is unfortunately missleading readers. There is however one common author with dedalus paper, I guess there are some incentives to leverage dedalus.

https://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-173.pdf

I am trying to do a survey of research and other works around TLA+, would be grateful to get some help from the community. For example, 

when examining two flagship HPC conferences, IPDPS and HPDC, there is only one paper (Reliability and Variability. MANA for MPI: MPI-Agnostic Network-Agnostic Transparent Checkpointing. HPDC'19) with a paragraph on system verification using TLA+ (with the specification not published).

Regards,

Ovidiu

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/SJ1PR21MB3723E82E74052A8F07205507B8CD2%40SJ1PR21MB3723.namprd21.prod.outlook.com.