[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Dedalus versus TLA+
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
--
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1166e069-9bd7-4ff3-906d-3962512e6d7dn%40googlegroups.com.