Incomplete efforts to automatically discover, check, and/or explain properties of federated execution

[petervdonovan]

This post includes the results from the project that I worked on last semester. I am posting about it now because the project is about to be indefinitely shelved and because I hope the statements that I formulated and empirically checked might be relevant to people who are currently using axioms about federated execution or who are currently documenting how it works in detail.

---

I feel that some discussions about federated execution are hindered by the following challenges:

• Although the general idea of what should be true about federated execution is not so hard to explain, properties that people try to specify sometimes turn out to have corner cases.
• Federated execution is time-consuming to manually document. Partly this is because of the easy-to-forget corner cases, which take time to find and remember, and partly it is because the implementation changes quickly, which gives documentation a tendency to go out of date.
• Because of the subtlety of some aspects of federated execution, it is sometimes necessary to state properties of federated execution very formally in order to avoid imprecision or ambiguity. However, this constraint is sometimes in tension with the other constraint that statements about federated execution have to be intuitive to everyone in order to establish shared ownership of the design and the code.

Because these challenges make it difficult for many of us (including me) to make true statements about federated execution without making any mistakes, I am under the impression that this has led to an attitude of skepticism about even basic facts about federated execution.

Documenting federated execution manually seems like a great idea to me, but because of the challenges, I am interested in and excited about automated ways of discovering or checking properties of the implementation. Such techniques might supplement or help us validate manual documentation.

Currently, I think that my (still incomplete) work here can at least kind of help us do the following:

1. Collect and serialize a whole bunch of reasonably diverse observations about the possible orderings of trace events in the RTI. (that is the protocol-test directory of the repo together with the ordering-server directory)
2. Manually express properties which characterize the pairwise orderings among various events (this is the trace-ord directory)
3. Automatically check whether those properties hold in all of the observations (this ugly function)
4. Quantify how much the properties "say" about our test cases, based on how many pairs of tracepoints the properties cannot show to be ordered with respect to each other (this quantity is measured using this code). (Details about the ordering in section 3 here, where it explains the use of the ≺ symbol; the same PDF is also linked below. The meaning of this ordering is also reflected in the natural-language explanations linked below)
5. Automatically generate easy-to-understand natural-language explanations of what the properties mean (the explain directory, which is currently in the explain feature branch)

My dream is basically to be able to produce correct, meaningful statements about federated execution automatically. Arguably the biggest missing piece here is the program synthesis aspect of it, for automatically generating the logical properties instead of writing them manually; I still think this is possible but while I was trying to implement it I got bogged down in complicated refactorings. I realize that this (specification mining and program synthesis) is already a pretty well-trodden path (i.e., lots of prior work), and in the foreseeable future I'm not even trying to write a paper about it.

This workflow is discussed in more detail in this PDF, which I warn you is a school report that was written in a bit of a rush and that has not been well-edited. I wouldn't really recommend reading it from start to finish, but I'm sharing it anyway in case anyone wants explanation.

The natural-language explanations are here. The fact that they are LLM-generated is partly just for fun, but it is also because I wanted to make sure that everything was explained well enough that the LLM would be able to "understand" the basic ideas and re-explain them back to me. A lot of the machine-generated explanations are wrong, but overall I feel happy about them. The explanations partially relieve the reader from having to interpret the ugly syntax that I made up ad-hoc to try to express the logical rules. Additionally, because the explanations are generated by an LLM with a low temperature parameter, they are not as idiosyncratic or as pointlessly obscure as they would have been if I had written them myself. I think these explanations are actually helpful, with the caveats that:

• the statements were true as of November or December 2023, and federated execution has changed since then. I'm happy to spend some time bringing the repo up to date with the latest master if anyone thinks that would actually be helpful
• the PDF has a table of contents (accessible using the table-of-contents feature of most PDF viewers, including the PDF viewers in Google Chrome and Firefox) because it would be too tedious to read the whole thing from start to finish
• in particular, the parts labeled "In-depth syntactic explanation" are too tedious for a human to read except as a way to debug where the LLM got confused and went wrong, or as a way to clarify specific confusions about the meaning of the formulas
• everything should be taken with a grain of salt, even though I went through all of it and annotated it according to how correct I thought the various parts are. Some of the text has confusions about concepts such as what is real vs. what is simulated and I hope we can avoid getting too bogged down with those sorts of mistakes.

[edwardalee]

This looks really interesting. The links to the PDF and natural language descriptions don't work for me. Perhaps forgot to push the files?

[petervdonovan]

I think that's fixed now (post edited above). GitHub seems to have something bad going on on their backend and their "attach files" feature just isn't working for me right now -- so I used a hacky workaround.