Generated Code Conformance Checking

[fhackett]

Related to #122, this is an idea about how to verify that PGo-generated code actually does what the model says it does.

Key idea: encoded into an MPCal model, there exists a mapping from reads/writes involving archetype resources to a form of model state. This mapping is either an identity mapping, or it is one of the mapping macro forms.

Therefore, TLC model state can be (almost) deterministically reconstructed from an ordered log of the archetype resource reads and writes performed by every critical section involved in a system's operation. PGo-generated code can be instrumented to generate such information automatically, and it seems plausible that a close-to-automatic process could then convert this information to a graph of TLC states, at which point conformance checking against the original MPCal model might be performed.

Success of such a check on a collection of real execution traces would go a long way toward indicating that an implementation really does match a specification, and, with the right API, this use case might not be limited to systems generated by PGo.

Additional comments:

• If we're comparing against an MPCal model, conformance could either relate to the model properties still holding, or, more basically, to the trace matching some valid exploration of model state. The latter might be easier to perform automatically, as it would not rely on specific assumptions that property formulations might make about how the model is laid out for TLC (node counts, etc).
• It's worth noting that, if the ongoing rewrite works out as hoped, TLC might not be the only way to perform checking. A lightweight ad-hoc program (combined with an AST interpreter for value-level TLA+) might be sufficient, if the goal is just to check that a partially ordered sequence of critical sections (including fully modeled state variables) is a plausible execution of a given model.

[lemmy]

Note that related to the last item, TLC has a simulator/generator mode.

[bestchai]

@lemmy, thanks for the quick comment. Is it possible to influence/direct TLC during simulator mode -- i.e., to push it along a concrete path that we are checking?

[lemmy]

@bestchai The simulator honors state and action constraints. https://github.com/lemmy/PageQueue/blob/master/Schedules.tla is an example of how to make TLC follow a specific schedule.