e2e testing approach

[lemmy]

We connected the implementation of CCF to the Ongaro-based (TLA+) specification for end-to-end testing. It made us discover serious bugs. A similar approach is currently being contributed to etcd. If you're interested in giving it a try, I'd be happy to discuss it with you."

[eatonphil]

Hey Markus! That looks fantastic! I'd certainly like to give it a try. It is a little bit early today since I still have a few more spots to implement (that I know don't work).

If I understand it correctly, I integrate your tracing framework which will generate a TLA+ spec that can then be checked by a TLA+ model checker? If so, then my main question I think is how do I integrate the tracing framework?

[lemmy]

Sorry for not being clear. There is no automatic generation involved. The main objective of the tracing framework is to leverage a human-written TLA+ specification when writing its implementation (in any programming language). In addition, it will keep the specification and the code in sync longterm. In the context of CCF, we "abused" tracing to fully align a reverse-engineered, incomplete TLA+ specification with the code. tlaplus/Examples#75 is more true to tracing's main goal. It documents the process of deriving an implementation from a specification.

Fortunately, in the case of raft-rs, we already have Ongaro's specification. To connect it with the Rust implementation, we would need to do the following:
a) Add logging functionality to the Rust code similar to microsoft/CCF@4c6ebee#diff-4e61c67c4990874cc31cb6f8cd91e4abe7506492fce0f73a4705d556d6861a42.
b) Fork and amend a trace specification such as https://github.com/microsoft/CCF/blob/main/tla/consensus/Traceccfraft.tla.

[eatonphil]

I might be misusing your words too, apologies. I get the part about logging, but it seems like the point of the logging is to produce another TLA+ spec that can be model checked. Is that not the case?

[lemmy]

The point of logging is to record a set of execution traces T and check T \subseteq Spec, i.e., check that the set of behaviors defined by a behavior specification (in TLA+) of that system.

[eatonphil]

Got it! So you produce a set of logs and you can verify if those logs match up to the existing Raft TLA+ spec.