Module Rig.Claim

A function may donate an input that dies with the call, such as an array operation's. A donation is safe only if nothing else reads the memory, and claims record what does. A claim lasts as long as its holder keeps it, and every view and borrow of an allocation shares the allocation's claims.

• A read claim marks an allocation as being read. The host holds one during Buffer.read and Buffer.write, and Claim.with_ on every buffer it is given. A hold (Claim.hold) is a read claim that lasts until Claim.release ends it or its value is unreachable, and that no consumption ends. submit holds one on every allocation the work uses until it returns, and a copy, blit or fill (Copying) on its buffers until it returns. Work on a device holds none, since the stamps order a write in place after that work.
• Only Claim.with_ holds memory exclusive, for an input its call donates, until it consumes the memory. Every other claim is a read claim.
• Memory that something outside rig can read or write is outside the claims and never exclusive. This holds for memory Buffer.of_bigarray and Buffer.of_io make, memory Buffer.export exported, memory Buffer.dma described or refused, and memory Claim.share marked. Memory that admits only Read (Buffer.access) is never exclusive either.
• Claim.consume consumes an allocation. A call that uses a dead buffer's bytes raises Invalid_argument with the reason given to the consumption. Consuming frees nothing, and the memory lives on in the buffer that Claim.consume returns. Where the memory was held exclusive, that buffer admits writes, its holder may write it in place, and no holder of a buffer made before the consumption sees the write. Code that the holder hands the new buffer sees the write, so the holder must order that code's accesses as for a buffer it made. Otherwise another claim reads the memory, and the buffer admits only Read (Buffer.access), so the bytes that claim reads are never written through it.

Taking a claim never waits. A read claim on memory held exclusive raises Invalid_argument, and a donated input whose memory another claim holds gets a read claim only.

Which inputs a function donates is part of that function's contract, and the function decides alone. A caller that passes a buffer to such a function and still needs its bytes holds a read claim on it across the call. The donation then stays a read claim, the function writes its result elsewhere, and the bytes stay as they were. Whether the caller's buffer stays live is the function's contract too: a function that consumes its input kills the buffer under any claim.

A host reader of memory that another domain may donate uses Buffer.read, which claims before it waits, since a claim taken after Buffer.wait returns leaves a moment in which the donation writes the memory. Host code over several buffers waits for them (Buffer.wait) inside a Claim.with_ that reads them. Where no other domain may donate the memory, the reader may use Buffer.wait.

A prepared submission holds its fixed memory and the buffers its parts name for its life (Submission.make). It claims the buffers of a run only while a submit runs. A donation between two submits can consume one of them, and the next submit with it then raises Invalid_argument for the dead buffer. A library that keeps buffers it does not own over its submits holds them (Claim.hold) for as long as it keeps them, or passes their memory to Claim.share.

A donor takes its inputs with Claim.with_. It consumes an input it holds exclusive before it uses it, since every call that touches the bytes of memory held exclusive raises Invalid_argument. While its function runs, the donor uses the buffer that Claim.consume returns as a buffer it made. It may write it from the host, copy into it, submit work on it, export it or share it. A donor of one input, or of an input whose buffers lie on several devices, consumes it only where it holds every buffer exclusive:

  Claim.with_ ~read:[] ~donate:bs (fun c ->
      if List.for_all (Claim.exclusive c) bs then
        Some (List.map (Claim.consume c ~why) bs)
      else None)

The buffers Claim.consume returns may be written in place after Claim.with_ returns.