How to document logical proofs against race conditions?

Question

Specific Background

I'm writing a library to extend the async backbone of a language with cooperative multitasking. (The language is Hack, but C# also implements async-await with Task, if the concept sounds familiar.) I've been able to express what I intend the library to do in code. The problem of the hour is when.

Some features of the language have well-defined behaviors with respect to order. I need this to put bounds in time around when things have a non-zero chance of resuming after they yield control (via await). However, the underlying scheduler is opaque to the program. Except for a very weak mechanism to push to the back of the scheduler (\HH\Asio\later()), when many tasks are complete simultaneously, control could return to any code awaiting one of them. Without care, this is a perfect recipe for race conditions and I've already discovered that the hard way.

I've written something of a spec to describe what ordering properties I want. I know the guarantees that come from all the well-defined behavior together are strong enough to enforce it. However, the most natural way I've found to propagate the guarantees is by logical proof. I am unsure, leaning towards doubtful, that the code structure alone can communicate the ordering guarantees, since the action of the well-defined properties is global-ish by nature, which couples an uncomfortable amount of code together.

General problem

I want to write documentation that outlines proofs of time-ordering that build on well-defined properties of language constructs. Because undefined behavior is just that — undefined — and because in my case the scheduler is opaque, tests don't say much. The propagation of guarantees are highly coupled to the implementation; tests could be passing on luck.

This is the subject of other questions too, and the consensus seems to fall between:

1. Not testing
2. Prying open the scheduler and testing

The latter isn't an option here, but to supplement the former, I have proofs of features of my spec given the implementation that I've written (it helps that async-await is more constrained than free multithreading). However, I am concerned this approach to documentation is unacceptably fragile because it is too tightly coupled to the implementation.

If this is a viable approach, how can I minimize fragility? If not, is there an example or resource I can look to where the code is expressive enough on its own?

Answer 1

First, I would document the library as you would any other public API: using descriptions of the abstractions and members. Try to include an introductory section with examples of how to use your library.

Secondly, I would add to the reference section the information needed for other developers to create their own informal proofs when using your library: pre-conditions, post-conditions, and invariants.

Finally, in an appendix, you can include the proofs. If they are formal proofs, it is difficult to avoid being entirely dependent on the implementation. If they are informal proofs, you may be able to base them on the pre-conditions, post-conditions, and invariants used in your implementation. This will be less detailed and less fragile than proofs based on every line of code in the implementation.

Finally, you might want to look for an automated proof checker you can use.