I don't know if this answers your question. I feel like it is about enumerating the possible states your program can be in. You could model it in TLA+, which i

I don't know if this answers your question. I feel like it is about enumerating the possible states your program can be in. You could model it in TLA+, which is about Temporal Logic of Actions; a good fit for modeling the happens-before. There are some nice visualizations associated with a checked model: https://www3.hhu.de/stups/prob/index.php/State_space_visualization_examples https://www3.hhu.de/stups/prob/index.php/State_space_visuali...