Flyology API reference

Description

Provides positional file I/O with lane-specific blocking behavior.

Example:

File := Flyology.IO.Files.Open ("state.bin");

Cancellation_Token

subtype Cancellation_Token is Flyology.Cancellation.Token;

Shared one-shot token. The token must outlive every operation using it.

Close

procedure Close (File : in out File_Descriptor)

Close File and set it to Invalid_File. Closing Invalid_File is harmless.

Parameters

File: Descriptor whose ownership is released

Raised exceptions

Device_Error: close(2) reports an error; File is invalidated

File_Descriptor

type File_Descriptor is private;

Owned operating-system file handle. This type is not controlled: the owning task must call Close. Concurrent operations require external synchronization, especially if Close may run at the same time.

File_Offset

type File_Offset is range 0 .. Interfaces.C.long_long'Last;

Nonnegative byte position used by positional reads and writes.

File_Operation

type File_Operation is abstract new Flyology.Operations.Operation with private;

Common limited base for completion-driven positional file operations. Concrete operations either borrow an aliased array or own a moved unique-buffer token until Finish consumes the terminal result. Scoped file operations currently require a lightweight owner; the existing synchronous overloads remain available in both lanes.

Finish

procedure Finish (Operation : in out Read_Operation; Last : out Ada.Streams.Stream_Element_Offset)

Consume a terminal positional read and publish its Last value.

Parameters

Operation: Terminal read operation
Last: Last element read, or Item'First - 1 at end of file

Raised exceptions

Device_Error: Submission or completion failed
Operation_Cancelled: Cancellation reached terminal state
Timeout_Error: Deadline cancellation reached terminal state

Finish

procedure Finish
  (Operation : in out Read_Operation; Item : in out Flyology.Buffers.Unique_Buffer; Read : out Natural)

Consume an owning positional read, move its buffer into vacant Item, and publish the new readable length. The move also occurs before a retained provider exception is raised.

Parameters

Operation: Terminal owning read operation
Item: Vacant buffer handle from the same pool
Read: Number of bytes read; zero at end of file

Raised exceptions

Program_Error: Item is occupied, belongs to another pool, or Operation does not own a buffer

Finish

procedure Finish (Operation : in out Write_Operation; Last : out Ada.Streams.Stream_Element_Offset)

Consume a terminal positional write and publish its Last value.

Parameters

Operation: Terminal write operation
Last: Last element written, or Item'First - 1 when none

Raised exceptions

Device_Error: Submission or completion failed
Operation_Cancelled: Cancellation reached terminal state
Timeout_Error: Deadline cancellation reached terminal state

Finish

procedure Finish
  (Operation : in out Write_Operation; Item : in out Flyology.Buffers.Unique_Buffer; Written : out Natural)

Consume an owning positional write, move its buffer into vacant Item, and publish the transferred byte count. The move also occurs before a retained provider exception is raised.

Parameters

Operation: Terminal owning write operation
Item: Vacant buffer handle from the same pool
Written: Number of bytes written on normal return

Raised exceptions

Program_Error: Item is occupied, belongs to another pool, or Operation does not own a buffer

Invalid_File

Invalid_File : constant File_Descriptor;

Sentinel denoting no open file.

Open

function Open
  (Path : String; Mode : Open_Mode := Read_Only; Create : Boolean := False; Truncate : Boolean := False)
   return File_Descriptor

Open Path directly on the calling lane. Create adds the platform create flag and Truncate truncates an existing file. Truncate is invalid with Read_Only. Open and Close are metadata syscalls and may block either lane's underlying thread.

Parameters

Path: Filesystem path
Mode: Requested access mode
Create: Create the file when it does not exist
Truncate: Truncate the file before returning

Return value

Newly owned file descriptor; the caller must Close it

Raised exceptions

Device_Error: The mode combination is invalid or open(2) fails

Open_Mode

type Open_Mode is (Read_Only, Write_Only, Read_Write);

Access requested from Open.

Enumeration literals

Read_Only: Permit reads only
Write_Only: Permit writes only
Read_Write: Permit both reads and writes

Operation_Cancelled

Operation_Cancelled : exception renames Flyology.Cancellation.Operation_Cancelled;

Raised only after a cancellation request reaches a terminal state and the caller may safely reuse its I/O buffer.

Read_At

function Read_At
  (Set     : not null access Flyology.Operations.Completion_Set'Class;
   File    : File_Descriptor;
   Offset  : File_Offset;
   Item    : in out Flyology.Buffers.Unique_Buffer;
   Timeout : Duration := Flyology.IO.Infinite) return Read_Operation

Start one positional read after moving Item into the operation. Item is vacant on return. Typed Finish moves the buffer back only after the kernel has relinquished it; abandoning the operation drains and releases the owned buffer to its pool. Item's pool must outlive the operation.

Parameters

Set: Completion set that owns the operation slot
File: Open descriptor permitting reads
Offset: Starting byte position
Item: Acquired destination buffer whose ownership transfers
Timeout: Relative operation deadline

Return value

Started limited owning read operation

Read_At

function Read_At
  (Set     : not null access Flyology.Operations.Completion_Set'Class;
   File    : File_Descriptor;
   Offset  : File_Offset;
   Item    : not null access Ada.Streams.Stream_Element_Array;
   Timeout : Duration := Flyology.IO.Infinite) return Read_Operation

Start one completion-driven positional read without parking the owner. Set, File, and Item must outlive the returned operation. Item is exclusively borrowed until Finish or finalization drains cancellation.

Parameters

Set: Completion set that owns the operation slot
File: Open descriptor permitting reads
Offset: Starting byte position
Item: Aliased destination buffer
Timeout: Relative operation deadline; zero makes one immediate completion attempt and negative means none

Return value

Started limited read operation

Read_At

procedure Read_At
  (File   : File_Descriptor;
   Offset : File_Offset;
   Item   : out Ada.Streams.Stream_Element_Array;
   Last   : out Ada.Streams.Stream_Element_Offset;
   Token  : access Cancellation_Token := null)

Read at Offset without changing the descriptor's file position. A lightweight task suspends until kernel completion; a native task blocks its thread in pread. A requested token is observed before native pread starts, but cannot interrupt a native syscall already in progress. A lightweight cancellation stays suspended until the kernel relinquishes Item, so Operation_Cancelled is a terminal buffer-ownership handoff. This is a potentially blocking operation and must not be called inside a protected action: a lightweight caller there raises Program_Error before Item is submitted, and native tasks keep stock behavior.

Parameters

File: Open descriptor permitting reads
Offset: Starting byte position
Item: Destination buffer
Last: Last element written, or Item'First - 1 at end of file
Token: Optional one-shot cancellation token

Raised exceptions

Device_Error: Submission, completion, or pread reports failure
Operation_Cancelled: Token cancellation reaches a terminal state
Program_Error: Lightweight caller is inside a protected action

Read_At

procedure Read_At
  (File    : File_Descriptor;
   Offset  : File_Offset;
   Item    : out Ada.Streams.Stream_Element_Array;
   Last    : out Ada.Streams.Stream_Element_Offset;
   Timeout : Duration;
   Token   : access Cancellation_Token := null)

Read positionally within one relative deadline. A lightweight timeout requests kernel cancellation and does not return until the kernel has relinquished Item. A native pread cannot be interrupted after entry, so timeout delivery may be delayed until that syscall returns. Negative Timeout waits without a deadline. Zero is one immediate attempt whose result wins, matching Flyology.IO.Wait and Flyology.Buffers.Acquire_For: a positional read has no readiness wait, so the attempt runs and returns transferred bytes, end of file, or a failure rather than Timeout_Error. Zero still bounds only readiness, not device latency, so a page-cache miss may occupy the caller for the duration of the disk read.

Parameters

File: Open descriptor permitting reads
Offset: Starting byte position
Item: Destination buffer
Last: Last element written, or Item'First - 1 at end of file
Timeout: Maximum monotonic wait in seconds
Token: Optional one-shot cancellation token

Raised exceptions

Device_Error: Submission, completion, or pread reports failure
Operation_Cancelled: Token cancellation reaches a terminal state
Timeout_Error: Deadline cancellation reaches a terminal state; never raised for a zero or negative Timeout
Program_Error: Lightweight caller is inside a protected action

Read_At

procedure Read_At
  (File      : File_Descriptor;
   Offset    : File_Offset;
   Item      : in out Flyology.Buffers.Unique_Buffer;
   Timeout   : Duration := Flyology.IO.Infinite;
   Operation : in out Read_Operation)

Start or restart one owning positional read.

Parameters

File: Open descriptor permitting reads
Offset: Starting byte position
Item: Acquired destination buffer whose ownership transfers
Timeout: Relative operation deadline
Operation: Fresh, released, or consumed read operation

Read_At

procedure Read_At
  (File   : File_Descriptor;
   Offset : File_Offset;
   Item   : in out Flyology.Buffers.Unique_Buffer;
   Read   : out Natural;
   Token  : access Cancellation_Token := null)

Read directly into an acquired unique buffer and replace its readable length. Kernel ownership and cancellation semantics match the array overload.

Parameters

File: Open descriptor permitting reads
Offset: Starting byte position
Item: Acquired destination buffer
Read: Number of bytes read; zero at end of file
Token: Optional one-shot cancellation token

Raised exceptions

Device_Error: Submission, completion, or pread reports failure
Operation_Cancelled: Cancellation reaches a terminal state
Program_Error: Lightweight caller is inside a protected action

Read_At

procedure Read_At
  (File    : File_Descriptor;
   Offset  : File_Offset;
   Item    : in out Flyology.Buffers.Unique_Buffer;
   Read    : out Natural;
   Timeout : Duration;
   Token   : access Cancellation_Token := null)

Read positionally into a unique buffer within one relative deadline. Timeout, cancellation, and terminal buffer ownership match the array overload, including the zero-Timeout immediate attempt.

Parameters

File: Open descriptor permitting reads
Offset: Starting byte position
Item: Acquired destination buffer
Read: Number of bytes read; zero at end of file
Timeout: Maximum monotonic wait in seconds
Token: Optional one-shot cancellation token

Raised exceptions

Device_Error: Submission, completion, or pread reports failure
Operation_Cancelled: Token cancellation reaches a terminal state
Timeout_Error: Deadline cancellation reaches a terminal state; never raised for a zero or negative Timeout
Program_Error: Lightweight caller is inside a protected action

Read_At

procedure Read_At
  (File      : File_Descriptor;
   Offset    : File_Offset;
   Item      : not null access Ada.Streams.Stream_Element_Array;
   Timeout   : Duration := Flyology.IO.Infinite;
   Operation : in out Read_Operation)

Start or restart a positional read in an established operation object.

Parameters

File: Open descriptor permitting reads
Offset: Starting byte position
Item: Aliased destination buffer
Timeout: Relative operation deadline
Operation: Fresh, released, or consumed read operation

Read_Operation

type Read_Operation is new File_Operation with private;

Scoped completion-driven positional read.

Timeout_Error

Timeout_Error : exception renames Flyology.IO.Timeout_Error;

Raised after a timed file operation's abort has reached a terminal state and the caller may safely reuse its buffer.

Write_At

function Write_At
  (Set     : not null access Flyology.Operations.Completion_Set'Class;
   File    : File_Descriptor;
   Offset  : File_Offset;
   Item    : in out Flyology.Buffers.Unique_Buffer;
   Timeout : Duration := Flyology.IO.Infinite) return Write_Operation

Start one positional write after moving Item into the operation. The readable payload length bounds the write.

Parameters

Set: Completion set that owns the operation slot
File: Open descriptor permitting writes
Offset: Starting byte position
Item: Acquired source buffer whose ownership transfers
Timeout: Relative operation deadline

Return value

Started limited owning write operation

Write_At

function Write_At
  (Set     : not null access Flyology.Operations.Completion_Set'Class;
   File    : File_Descriptor;
   Offset  : File_Offset;
   Item    : not null access constant Ada.Streams.Stream_Element_Array;
   Timeout : Duration := Flyology.IO.Infinite) return Write_Operation

Start one completion-driven positional write without parking the owner. A terminal cancellation does not roll back bytes already written. Set, File, and Item must outlive the returned operation, and Item must not be changed until Finish or finalization drains cancellation.

Parameters

Set: Completion set that owns the operation slot
File: Open descriptor permitting writes
Offset: Starting byte position
Item: Aliased source buffer
Timeout: Relative operation deadline; zero makes one immediate completion attempt and negative means none

Return value

Started limited write operation

Write_At

procedure Write_At
  (File   : File_Descriptor;
   Offset : File_Offset;
   Item   : Ada.Streams.Stream_Element_Array;
   Last   : out Ada.Streams.Stream_Element_Offset;
   Token  : access Cancellation_Token := null)

Write at Offset without changing the descriptor's file position. A single call may transfer fewer than Item'Length elements. Lightweight tasks suspend for kernel completion; native tasks block in pwrite. Token and buffer-lifetime semantics match Read_At. Cancellation does not roll back bytes already written. When Operation_Cancelled is raised, Last has no defined application meaning and a blind retry may duplicate or overwrite data; callers needing retry safety must provide an idempotent protocol or track committed offsets independently. Like Read_At, this must not be called inside a protected action; a lightweight caller there raises Program_Error before Item is submitted.

Parameters

File: Open descriptor permitting writes
Offset: Starting byte position
Item: Source buffer
Last: Last element written, or Item'First - 1 if none, meaningful only on normal return
Token: Optional one-shot cancellation token

Raised exceptions

Device_Error: Submission, completion, or pwrite reports failure
Operation_Cancelled: Token cancellation reaches a terminal state
Program_Error: Lightweight caller is inside a protected action

Write_At

procedure Write_At
  (File      : File_Descriptor;
   Offset    : File_Offset;
   Item      : in out Flyology.Buffers.Unique_Buffer;
   Timeout   : Duration := Flyology.IO.Infinite;
   Operation : in out Write_Operation)

Start or restart one owning positional write.

Parameters

File: Open descriptor permitting writes
Offset: Starting byte position
Item: Acquired source buffer whose ownership transfers
Timeout: Relative operation deadline
Operation: Fresh, released, or consumed write operation

Write_At

procedure Write_At
  (File    : File_Descriptor;
   Offset  : File_Offset;
   Item    : Flyology.Buffers.Unique_Buffer;
   Written : out Natural;
   Token   : access Cancellation_Token := null)

Write directly from a unique buffer's readable payload. Item remains owned until the synchronous call returns.

Parameters

File: Open descriptor permitting writes
Offset: Starting byte position
Item: Acquired source buffer
Written: Number of bytes written on normal return
Token: Optional one-shot cancellation token

Raised exceptions

Device_Error: Submission, completion, or pwrite reports failure
Operation_Cancelled: Cancellation reaches a terminal state
Program_Error: Lightweight caller is inside a protected action

Write_At

procedure Write_At
  (File      : File_Descriptor;
   Offset    : File_Offset;
   Item      : not null access constant Ada.Streams.Stream_Element_Array;
   Timeout   : Duration := Flyology.IO.Infinite;
   Operation : in out Write_Operation)

Start or restart a positional write in an established operation object.

Parameters

File: Open descriptor permitting writes
Offset: Starting byte position
Item: Aliased source buffer
Timeout: Relative operation deadline
Operation: Fresh, released, or consumed write operation

Write_Operation

type Write_Operation is new File_Operation with private;

Scoped completion-driven positional write.