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.
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:
- Not testing
- 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?