3

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?

  • 1
    Sounds much like the lock order problem: you do need to document the lock order to avoid deadlocks, but where to put the documentation? I suggest a separate design document. If you like most coders prefer ASCII so that it can be put under version control painlessly, use a text file or if you want better formatting, use LaTeX. – juhist Mar 5 '17 at 7:31
  • @juhist I'm guessing some of this is a matter of style, but do lock order documents tend to be explanatory of the codebase, or do they read more like guidelines? I haven't worked with locks before, so I've never read a document like this, but it tackles exactly the same nature of problem by the sounds of it. – concat Mar 6 '17 at 2:30
  • It is unclear to me if you wish the documentation to communicate the proof of the behavior of the library, or the documentation is to be used by the library user to understand how it is to be used. If there is a potential for race conditions, ideally the library API would be designed in such a way that the default, most likely usage, minimizes that potential. Documentation is frequently ignored. – Frank Hileman Mar 6 '17 at 17:05
  • @FrankHileman The former. I hope it fills the void that the unwriteability of tests leaves behind. – concat Mar 6 '17 at 17:34
  • I am glad you are doing proofs and pointing out to people that tests cannot be done. It is too often that test results are taken as "proof". However, the average programmer is unlikely to read your proofs. – Frank Hileman Mar 6 '17 at 17:42
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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.