componolit / gneiss Goto Github PK
View Code? Open in Web Editor NEWFramework for platform-independent SPARK components
License: GNU Affero General Public License v3.0
Framework for platform-independent SPARK components
License: GNU Affero General Public License v3.0
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:
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.
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:
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:
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:
Some ideas:
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:
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:
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 successRetry
: in case of a temporary errorUnsupported
: in case of an unsupported operationToo_Large
: in case the request length is to largeThe 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.
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.
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:
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 (obsoleted by new interface, cf. #69)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.
A similar problem exists for the block server. While the (obsoleted by new interface, cf. #69)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.
The block dispatcher provides a session label with the (moved to #50).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
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.