Elaborate on contracts

[polytypic]

This PR "tightens" the wordings on the requirements for schedulers when implementing the Picos effects.

The words "must" and "should" are now used more intentionally.

The biggest change is that the Spawn effect should now be all or nothing — if spawn returns normally, the scheduler should guarantee that all the mains spawned will be called and if spawn raises no mains should be called. This is how the sample effects based schedulers have worked already (modulo running out of memory) and this requirement has crossed my mind earlier, but for some reason I had failed to spell it out explicitly. This PR also changes Picos_threaded to provide the same guarantee as much as possible. The reason behind this is that otherwise it becomes very tricky (impossible even) to ensure that all spawned fibers are accounted for and no resources are leaked. OTOH, with this guarantee, it is safe to e.g. increment a counter before attempting spawn and then decrement it either in the fiber or in an exception handler:

Atomic.incr live_child_count;
try
  Fiber.spawn ~forbid:false computation [ fun () ->
    match main () with
    | () -> Atomic.decr live_child_count
    | exception error ->
      report_error error;
      Atomic.decr live_child_count
  ]
with exn ->
  Atomic.decr live_child_count;
  raise exn

In general, all of the effects are all or nothing.

Two of the effects are somewhat special when it comes to cancelation:

• As specified earlier already, the Current effect must not be discontinued. This is because current is used by programs to obtain the fiber handle through which cancelation propagation can be controlled and if current would raise, it would be much more difficult to control cancelation propagation.

• The Await effect also must not be discontinued. The scheduler must instead continue it with the cancelation exception (with backtrace). This is for performance, convenience, and to make the cancelation visible in the types — I expect calls of await are the places where cancelation requires extra care. Having the Await always return a value can be convenient in cases where one must deal with the possibity of cancelation while also juggling atomic state and cancelation propagation.

The motivation behind the requirements for schedulers is to make it possible to build non-trivial mechanisms, such as structured concurrency models and synchronization and communication primitives, on top of the effects correctly and efficiently.