fhackett
commented
3 years ago Some thoughts, after mulling over the noted challenges.
It seems that attempting to work backwards from plain TLA+ invariants, written in terms of the TLA+ output, may be an exercise in frustration.
By design, the variables involved in the TLA+ output may be significantly different from those available to the generated code... which means, if we want to go down this road, that we have another variation of the abstraction problem inherent to the problem PGo tries to deal with.
One way to address this issue might be to allow archetype-level invariants to be specified in MPCal, in terms of the archetype resources. This might allow an implementation to reasonably execute the invariants, but, in turn, would make it highly unclear what the TLA+ model should do... worse, the invariants might need to perform reads on the archetype resources (because that is the only way to access such things, at runtime), meaning that the assertions would destructively affect system state. This is also without beginning to ask what the TLA+ translation of such invariants might look like.
Clearly, the "obvious" solution has some issues, from a practical viewpoint. At a high level, the biggest roadblock might just be that, unlike the TLA+ spec, the implementation is not likely to have all the information it needs to ever check most interesting assertions (at least, in one centralised location).
All that being said, maybe the answer lies in ... well, how do you check distributed assertions at runtime? Distributed tracing + verification seems to be an answer, here. In that case, the challenge becomes:
- we still need to somehow correspond model state with some window into program state... it's unlikely that there will be a general solution to this, given the ad-hoc nature of all the encodings (in TLA+, in the resource implementations). Maybe we can require resource implementations to have a "verifier mode" where they describe their state in terms of the TLA+ model?
- we need to track progress of state / the overall algorithm across a distributed system, as verification conditions apply to some global system snapshot
Both of these things would not be unreasonable to do e.g using our distributed tracing lib, or something like it: https://github.com/DistributedClocks/tracing. The challenge would then be to map the outputs back to something that the verification conditions can "understand". This would require (1) obviously, generating something one could feed to a model checker, and (2) some care when writing those conditions. For instance, one might want to avoid depending strongly on overly conservative model checking assumptions (e.g some exact configuration of nodes, or a statically chosen set or overly restrictive model of input/output values), which would prevent the verification conditions from being applied to the more diverse set of scenarios that might occur during runtime.
So, this challenge seems to be more or less a runtime problem. It might be possible to somehow assist developers in writing appropriately abstract verification conditions, but, more or less, this is a case of needing to record system behaviour, format it for e.g TLC, and check that the properties are satisfied.
lemmy
It would be much easier to argue PGo's soundness, if generated programs could check themselves.
This issue suggests adding a flag to PGo, such that it attempts to extract safety properties from the TLA+, and compiles assertions of them into generated code. Temporal properties will likely not be practical to handle.
Challenges: