componolit / gneiss Goto Github PK

With the current implementation we run into many aliasing issues that are hard to fix. Due to the inadequacy of the aliasing checker (e.g. that globals are treated as atomics and that accesses are not distinguished between read/write) the approach of further splitting the data path does not work.

The only other option with the current implementation seems to be disabling some aliasing checks. But this is cumbersome as it has to be done by the user and furthermore dangerous as it might happen that an actual aliasing problem is hidden in disabled false positives.

The best option seems to be to remove the identifier/instance types completely and always pass the whole session object. This requires that only the passed session object is used but never the global.

To still be able to identify the caller of a callback the session should be tagged by the application. A tag can then be retrieved from the passed session in the callback and any decision (e.g. different return values for different callers) must be based solely on that tag but not on the global session object.

Further it might happen that multiple sessions of different types are used that all can be called in callbacks. To use a session of another type in a callback all sessions must be in separate constructs (separated by session type). If a session is in the same compound type as the session passed as argument aliasing will happen. This shouldn't be a problem as tags can be provided freely by the application (and therefore multiple times over multiple different session types).

The tag type is intended to fit into a 32bit unsigned value (similar to the request id of a block request).

The block server interface currently wakes up client implicitly after the callback returns on Genode. Yet this only works if the callback has been called from the servers own signal handler. If the callback is called from another signal handler (e.g. in a proxy component) the client won't be woken up.
To fix this a procedure Unblock_Client (S : Server_Session) will be introduced that has to be called by the application to wake up the client.

Furthermore the Initialize procedure of the server will additionally get the requested transfer size of the client. It is free reject a connection based on this information.

The CAI should be tested by the CI on all supported platforms. The test should as far as possible support the three steps:

• build
• prove
• run

Right now, a generic buffer type defined in Block is used for the Block.Client.Submit_Read and Block.Client.Submit_Write operations. We should make such functions generic in their buffer type to allow the user to chose which buffer type to use. The same is true for the to-be-implemented server interface.

Interface to retrieve a component-specific configuration which is a string of arbitrary format. The platform implementation has a well-known location for the configuration (Genode: ROM named "config", Muen: memory region named "config" (or similar), POSIX: environment variable named "CAI_CONFIG" ointing to file).

The config interface is realize as generic package with a procedure with a single in-parameter as formal parameter:

generic
   type Element is private;
   type Index is range <>;
   type Buffer is array (Index range <>) of Element;
   with procedure Parse (Data : Buffer);
package CAI.Configuration.Client
   function Create return CAI.Configuration.Client_Session;
   procedure Initialize (C : in out CAI.Configuration.Client_Session);
   function Initialized (C : CAI.Configuration.Client_Session) return Boolean;
   procedure Load (C : in out CAI.Configuration.Client_Session);
   procedure Finalize (C : in out CAI.Configuration.Client_Session);
end CAI.Configuration.Client;

For a completely asynchronous interface all sessions follow an approach using an event handler. There is no difference between a server or a client interface since both generate and handle events.

A session interface has the following minimal interface:

private with Cai.Internal.Session;

generic
   type State is limited private;
   with procedure Event (S : in out State);
package Cai.Session

   type Session is private;

   function Create return Session;

   procedure Initialize (S : in out Session; C : in out State);

   procedure Finalize (S : in out Session);

private

   type Session is limited record
      Cai.Internal.Session;
   end record;

end Cai.Session;

Each session state is implemented as a private record with an internal type. The internal type can be anything and is defined by the platform. Furthermore each session can (and should) implement additional functions that can be called with the Session type. This includes client function to call other sessions and polling functions to handle all events in the Event procedure.

Implement a state machine approach on top of our current (low-level) block client interface.

Migrate all tests an applications to the new interface.

• void pointers
• unnecessary indirections/encapsulations

The request type stores partially platform state and shouldn't be changed at the wrong place. To solve this issue it will be made private and only accessible via specific functions/procedures.

Add background on why CAI is needed, what the benefits are etc.

Implement sessions for the POSIX platform:

• Block client -> aio
• Log -> stderr
• Timer -> clock_gettime

Requires #32

The NBD server implements a block server session and exports if over a socket.

To provide better support for capability based system all sessions require an opaque capability object that is provided by the platform. This object resides in the package state and cannot be initialized there. The construct method receives an in out parameter with an initial value it can copy to its local state.

Components may wish to exit and signal a result of their execution to the platform. Add a platform interface to exit a component and to signal the exit status.

The NBD client enables access to an NDB server using a block client session.

The TRIM operation is beneficial for optimizing SSD storage. For Trim the request type is equivalent to Read/Write. The request is:

procedure Trim (D : in out Component.Block_Device; R : in out Request);

The latest interfaces changes were only implemented on Genode. They also need to be implemented on Linux and Muen.

The procedures Session_Request, Session_Accept, Session_Cleanup must only be called in the Dispatch procedure of the dispatcher. This is currently not enforced. To enforce this the Dispatch procedure will receive a limited private in paramter that is required to be passed to each of this three methods. As it is a limited private type it cannot be copied or stored outside the Dispatch procedure.

This interface allows users to request the current monotonic time (similar to Clock in Ada.Real_Time). We should also think about function to retrieve precision and bounds of the timer.

To allocate large memory regions that do not fit into the BSS an allocator is required. The allocation mechanism itself is platform dependent and is not required to be valid SPARK. The public platform independent interface looks as follows:

generic
   type T is private;
package Cai.Memory_Pool is

   pragma Elaborate_Body;

   Instance : T;

private

   Instance_Address : System.Address;

   for Instance'Address use Instance_Address;

end Cai.Memory_Pool;

An implementation on Genode would use the new keyword and implement __gnat_malloc on Genode:

package body Cai.Memory_Pool is

   type T_Access is access T;
   Instance_Access : T_Access := new T;
   use type System.Address;

begin
   if Instance_Address = System.Null_Address then
      Instance_Address := Instance_Access.all'Address;
   end if;
end Cai.Memory_Pool;

So far, we mainly supported the notion of programs with one Ada main loop that would do arbitrary things, sometimes block, sometimes poll for events. However, experience show that fully event-driven programs are much cleaner and performant. More importantly, when done right, such components avoid unnecessary state and back-pressure from clients. This is how components are supposed to be structured on Genode these days.

For Ada components following this pattern we need a couple of things:

• An interrupt-like mechanism to signal progress from the platform
• Interface to initialize a component and set up signal sources
• Interfaces that
  1. work in polling-mode upon reception of a signal
  2. allow for detecting the readiness of downstream components
  3. allow for rejecting a request if the component is not immediately ready to process it
• A strategy to implement that concept in an Ada main loop on platforms that do not directly support signals (e.g. Muen)

We should review the existing block-device interface to meet this pattern. For Genode, we have to create a component (akin to libc/component.h) that allows for easy setup of such event-driven Ada components.

(This topic was migrated from the last comment of Componolit/ada-runtime#22 where it didn't belong).

Call tests in the CBE repo actually should become CAI platform tests.

Once #24 is done, we can enable client tests in the CI. For server tests, we need to implement NBD and check whether this can be used on TravisCI.

At least, run gnatprove on the library and examples.

The implementations of block and configuration client on posix raised obscurities about the distinction of the posix/Linux platforms. The current posix implementation is a C implementation based on libc that uses standard posix mechanisms. Although parts of the code are Linux specific and will most probably not compile on other platforms. This raises the issue if posix is the correct platform definition.

I see three ways to solve this issue:

1. rename posix to linux
2. implement platform generic mechanisms
3. divide posix into more platforms with a large shared code base

Some ideas:

1. This is probably the easiest option. But it would collide with an eventual in kernel implementation which then also would be called linux.
2. Since all the code runs on posix conform platforms with posix conform build systems/compilers abstraction layers that provide implementations for different platforms could be embedded without changing the public interface of the posix platform for the CAI build system. In detail this means wrappers around the problematic code (in this case inotify and block size detection) that provided different implementations for different posix platforms which are selected via macros. These implementations could then be extended easily for new posix compatible platforms.
3. Basically like 2. but instead of macros the distinction is done via the CAI build system. Each posix directory would have a subdirectory for Linux/BSD etc. if necessary.

Personally I prefer 2.

When submitting larger amounts of packets the allocation fails with

Error: Uncaught exception of type 'Genode::Packet_stream_source<Genode::Packet_stream_policy<Block::Packet_descriptor, 256u, 256u, char> >::Packet_alloc_failed'

This doesn't seem to be taken into account by the ready function which checks if the submit queue can take more requests. Aside from the check I'm not sure if a signal handler is in place for "packets can be allocated again".

The client interfaces requires a generic operation that is called whenever an event happened on the platform side. A user of the client can instantiate the generic client package with that operation and the type of the state to be passed to the callback.

Generic parameters are:

• State type
• Callback function

In addition, the client package has an operation to update the state.

To run multiple consecutive tasks in a asynchronous environment a scheduling approach is required.
Each task is executed in an event handler that is called by the platform. When it has been called it will return eventually and be finished or not. If it is finished the scheduler should call the next task, if not it should return to the platform and wait for the next event. (Basically cooperative scheduling)

To realize this in SPARK generic packages can be used. Each task is an instance of the Task package that is instantiated with the procedure it executes and the next consecutive task (the last task is a special implementation that does nothing). To prevent overly nested packages instances are only implementation but not data-dependent. For a single implementation an array of instance objects is passed. Each task will then first execute the implementation for each instance before it will call the next task.

Instead of emulating a queue we should completely remove Update_Response_Queue and call Update_Request on all requests. Platforms that use a queue internally can implement this via a cache.

The generic packages get procedures as formal parameters that have implicit contracts. Currently these contracts cannot be annotated since the required functions are inside the generic package.
To overcome this problem all functions of the client and server packages should reside inside the parent package that also defines all required types and their property functions.

Furthermore the generics need to get a pre and postcondition function as formal parameter for each procedure and function they receive.

Also requests should be bound to a specific session on allocation and unbound on release.

Steps:

• move functions to parent package
• pre and post condition for generics
• bind request to specific session

Currently when a dispatcher gets a session request it checks if a free session is available and then calls accept with that session. Accept will then initialize it. This is fine as long as all initialization steps inside the server implementation work.

In the case of a failing initialization the client would then talk to an incomplete server (the server cannot initialize some of its parts, e.g. hardware or another server connection it is proxying to). To solve this problem The dispatcher and server interface should be changed:

The server interface should get a generic parameter function Initialize (S : Server_Instance) return Boolean which can be implemented. This represents the internal state of the server implementation.
Furthermore the Session_Accept procedure should only take sessions that are already initialized and there should be a procedure Session_Initialize that does all the initialization work (the platform part still needs to be initialized before the user defined part).
This makes sure that no incomplete sessions can exist.

Also this could lead to a session being accepted multiple times (since it is initialized in both cases). This could either be fixed by adding this property to the server interface or by checking that only sessions can be accepted that have been initialized in the same context (the session is uninitialized -> initialization -> accept, all in the same procedure).

Since the current directory structure requires building all interfaces for all platforms and furthermore makes it hard to add code that is shared by some but not all platforms a new structure is required:

src/
├─cai.ads
├─cai-types.ads
├─<cai-generic.ads>
├─log/
  ├─cai-log.ads
  ├─generic
    ├─cai-log.adb
  ├─<platform>
    ├─cai-log.adb

src will now contain only the specs that are generic to all interfaces. Each interface has its own subdirectory containing the specs and the platform independent bodies. For each platform a separate subdirectory exists in each interface. Futhermore interfaces can supply a generic platform that contains code shared by multiple platforms.

Provide CAI user with defined way to start a component.

Idea:

Provide a generic package CAI.Component which the user has to instantiate with a Construct procedure. This procedure is called during component startup to set up the component. The generic package defines a symbol that is the entry point of the component.

Currently procedures the procedures Allocate_Request, Enqueue and Acknowledge are allowed to fail. Failing means that the request status does not change.

For Acknowledge this is sufficient since any request can be acknowledged and the server cannot create or destroy requests by its own.

On the other hand Allocate_Request and Enqueue are called with requests created by the application that can be erroneous.

Allocate_Request needs at least a temporary/permanent error semantic. A temporary indicates that there are currently insignificant resources to allocate that request and that the application should try again later. A permanent error indicates that this set of arguments will never succeed in allocating the request, e.g. because the request type is not supported by the platform. In this case the application can stop retrying, or in case this operation is required, detect that it cannot proceed.

Enqueue is more difficult to decide. Either there is the guarantee that a request that can be allocated can also be enqueued. In this case the only possible error would be a full enqueue queue which is temporary. I currently cannot think of a scenario where enqueue would fail permanently (especially of one that cannot be catched by Allocate_Request.

An idea would be to extend Allocate_Request by one parameter showing the result:

procedure Allocate_Request (C : in out Client_Session;
                            R : in out Request;
                            ...
                            S :    out Result);

Where the result could be:

• Success: in case of success
• Retry: in case of a temporary error
• Unsupported: in case of an unsupported operation
• Too_Large: in case the request length is to large

The last one could also replace the Maximum_Transfer_Size function.

All interfaces should be a child of the CAI root package.

To consolidate the current implementation all tests and the platform code written in SPARK should be proven for the absence of runtime errors.

• test/hello_world
• test/rom
• test/timer
• test/block_client
• test/block_server
• test/block_proxy
• src/common/*strings
• src/common/*strings_generic
• src/log/client/genode/*log-client
• src/log/client/linux/*log-client
• src/log/client/muen/*log-client
• src/rom/client/genode/*rom-client
• src/rom/client/linux/*rom-client
• src/rom/client/muen/*rom-client
• src/timer/timer*
• src/timer/client/genode/*timer-client
• src/timer/client/linux/*timer-client
• src/timer/client/muen/*timer-client
• src/block/*block
• src/block/client/genode/*block-client
• src/block/client/linux/*block-client
• src/block/client/muen/*block-client
• src/block/server/genode/*block-server
• src/block/server/genode/*block-dispatcher
• src/block/server/genode/cxx-block-server
• src/block/server/genode/cxx-block-dispatcher
• src/block/server/muen/*block-server
• src/block/server/muen/*block-dispatcher
• src/platform/genode/*component
• src/platform/linux/*component
• src/platform/muen/*component
• src/platform/muen/*main
• src/platform/muen/*muen
• src/platform/muen/*muen
• src/platform/muen/*muen_registry
• src/platform/muen/*muchannel_reader
• src/platform/muen/*muchannel_writer

This list lists all units that should be proven. The * is only used to shorten componolit-interfaces-. The units are selected by all packages that have bodies or that implement expression functions if they don't have a body. Also all generic packages should be proven via the tests that use them.

The new client log interface assumes that we have one single connection to a log server that is already initialized when we start using it. We would not be able to implement, e.g. a log splitter with the current interface.

Our LOG session should get a Create function and an Initialize procedure as the block session. In Initialize we could then configure e.g. different log backends or target facilities.

Currently we pass requests to the Supported function. This does not make too much sense, as operations are either supported or they aren't and this does not change. Make Supported operate on operations instead.

Implement a session that triggers an event after a specific amount of time.

• events are relative (in X seconds)
• data type Duration
• One single oneshot timer is supported
• Timers can be overwritten

Currently we need a public type for the image functions of the log interface to cast own types. A more elegant solution is a generic function with a formal discrete type.

To prevent copying data multiple times the platform should make the required buffer available to the application by calling the application with a buffer argument.
The client will gain an additional formal parameter which is a procedure that receives the write buffer as out parameter. This out parameter directly points to the buffer.
Due to the ceasing requirement of a write buffer for the write request all enqueue procedures can be merged.
The same will apply to the read procedure. Instead of providing a buffer a callback is triggered that calls the read with a buffer as in parameter.
Furthermore the supported function will only check for the request type but not the whole request.

• async write via callback
• async read via callback
• supported only for request type

The initialization of the block buffer should accept a requested buffer size in bytes to determine its internal packet buffer. The maximal transfer size will then be the min(buffer size, device maximal transfer size from the server).

In the Genode platform implementation we use Block::Packet_descriptor::END to signal a SYNC request. Not sure whether this is right - check and remove if this does not denote a sync operation.

If we make SYNC a no-op on Genode, are we going to deliver a SYNC event with ERROR set? Or a syncable flag for the device?

When trying to build CAI on Genode to test the renaming of the Configuration interface I had to update Genode to 19.05 to use our latest runtime. This caused the block interface to break when building. We should check what work is required to make it work again (especially if we can fix it short time or if we have to use Genodes new block client interface from now on).

Document the following aspects of the interfaces:

1. How to use a client interfaces
2. How to implement a server interface
   • How to create a custom types package for server interface
3. How to support a new platform

There are currently some parts of the interface design that have redundant arguments, etc:

• In the block client interface an incoming response is retrieved by the Next function. if it is a read response the data can be retrieved by calling Read on this request. It then has to be acknowledged by calling Release after which the platform discards it. Both Read and Release require the request as argument although no other request than the one returned by Next is available for handling. Therefor it doen't need to be passed as an argument. (obsoleted by new interface, cf. #69)

• A similar problem exists for the block server. While the Discard procedure already doesn't take the request as argument the Read, Write and Acknowledge procedures do. They also depend on the request returned by Head which also implements a FIFO Queue so only the first element is available. Either the response path needs to be separated from the request path to provide the ability to acknowledge out of order (which is desirable) or only first request in the queue can be responded at a time. (obsoleted by new interface, cf. #69)

• The block dispatcher provides a session label with the Session_Request procedure. This label can be used to identify the requesting client. It is then passed to the Session_Accept procedure. Inbetween it could have been changed. Since Session_Accept uses the label to identify the actual session to connect the label shouldn't be changed as any other session is probably not available or cannot be safely connected to. This information should be instead passed via the dispatcher capability (moved to #50).