This is all the changes I've made to CubedOS this summer. I was using individual commits, but I apparently have been working on an outdated local branch for the last month and don't know git well enough to deal with that in under a day. Also this refactor turned out to be very iterative and I think including the full git history would be mostly confusing to viewers.
Changes to project structure:
I migrated the project to Alire. AdaCore has made clear that this is the future. I initially did this to gain access to the SPARK library, but that has not yet been released to Alire. It will be soon.
CubedOS is now a "Crate" or whatever AdaCore calls their packages
Changes to the message system:
Implementation Differences
Messages now reference a dynamically allocated payload of variable size. Merc doesn't yet take advantage of this yet, but payloads of any size are possible and not-dependent on any global configuration
Modules register with the message system on startup, specifying the size of their message queue, allowing per-module message queue sizes.
Several message related types were pulled out of Generic_Message_Manager into CubedOS.Message_Types. This resolves some circular dependency issues.
CubedOS now uses the Jorvik tasking profile
Removed pragmas to disable warnings about multiple queing on mailboxes
Created a separate Mutable_Message_Record. Message_Record is now immutable. This was intended to aid the decoder functions while making it harder for module writers to screw up and produce invalid messages. It's usefulness for that application is limited though. It's still useful in a few select places so I decided to keep it.
Added Debugging Feature
Message_Manager now may optionally be instantiated with a message debugger object which observes specified internal events of the message system and can produce debug information. These events include:
When all known modules in the system have been initialized
When a message is sent
The success/failure of a message to be queued in a destination mailbox
When a module reads a message from its mailbox
When a message is discarded because its type is incompatible with the destination module
Created two default implementations: a null debugger which does nothing and is suitable for production, and a console debugger which reports message info to the console.
Future developers may create custom extensions of message debugger for their needs
Domain and Module Addressing
Module IDs have been semantically changed:
In a multi-domain CubedOS system, a module ID is paired with exactly one module type. For example in a system with multiple domain each with an instance of the Time_Server module, the modules must have the same ID in both domains.
Module IDs are no longer required to occupy a continuous range.
A system may have at most 256 unique modules.
All domains in a system are defined in the name_resolver file by creating a Domain_Metadata constant which describes what modules are included in the domain, and the domain's number.
Generic_Message_Manager is instantiated with a domain metadata object, supplying the message manager with more information to check safety with.
Name_Resolver is now back to pre-domain syntax for assigning module IDs. Each module name is assigned a Module module ID instead of an address. If a module is in multiple domains, it's added in multiple domain metadata declarations.
Safety Improvements
All messages now have an associated Universal_Message_Type record which identifies a message type uniquely across domains and modules. This enables greater safety.
Modules declare statically what message types they may receive. The message system filters messages guaranteeing they receive only safe messages.
This is specified in the MXDR file, and the generated API files produce a Module_Metadata object containing this information which the module implements.
In many situations, modules can statically prove that sent messages are destined for modules which may receive them.
In situations where that isn't possible, unacceptable messages are discarded by the message system.
All modules wishing to send messages must do so with a Module_Mailbox object which uniquely identifies the sending module.
When modules register themselves with the message system, this allows us to check carnality and ensure that no two modules have the same ID. If there is a collision the program crashes immediately on startup.
The message system doesn't allow messages to be sent or received until either all modules known to be in the domain have registered, or the special debugging function Skip_Mailbox_Initialization is called. This prevents messages from being lost at startup before mailbox size is determined. This is also enforced by SPARK.
All sent messages are guaranteed to have a the correct sender address.
Message_Manager provides a Wait function which blocks until the system is ready.
Changes to Module Structure
Modules now must hold a Module_Mailbox object to use the messaging system. They shouldn't use the Fetch operation anymore.
They should all have an Init procedure which will be called from the Main procedure on startup which register's their mailbox.
They must wait for the message system to fully initialize before reading or sending messages. SPARK will help with this.
Changes to Transport Modules
Transport modules are not initialized like other modules.
They don't have a mailbox anymore.
Messages destined for a foreign domain will be recognized by the message manager and passed to a function defined in Domain_Config.adb which CubedOS systems must implement. This function will inspect the message and then give it to a transport module.
When a transport module receives a message from a foreign domain, it gives it to the message manager directly via the Handle_Received procedure.
Changes to Sample Programs
Updated the Networking sample to use the refactor and Merc generated MXDR files.
Changed the structure of the networking sample to be two projects, one for each domain instead of the confusing, environment variable related, probably I never figured it out, build system.
Updated the module templates to use MXDR files and the message refactor.
Changes to Core Modules
UDP Transport module now waits until the UDP port is connected before sending messages.
Changes to testing:
Added tests for XDR float and double implementation
Added tests for the bounded pointer queue
Added testing suite for message safety features
Removed message passing test (it wasn't declarative and was very confusing to follow and alter to support the refactor. Ended p rewriting it completely).
Added check_messaging_proof.adb. This is a manual test meant to verify that SPARK is providing appropriate feedback when attempting to read messages without proof that the message system is initialized.
Changes to the CubedOS Library:
Changes to XDR lib
Implemented the float and double decode functions. They are tested to be fully IEEE compliant. They have not been completely SPARK proven.
Added tentative Max_Time and Max_Time_Span constants to communicate the maximum supported time values in MXDR. This issue needs to be revisited in depth as I explain in the Merc repo https://github.com/cubesatlab/merc/issues/1
Added Bounded Queue Implementation
Created a bounded queue implementation in SPARK. It's pretty janky and not fully proven. I use it in the message manager to abstract the details of managing a queue. Overall, SPARK hates it and using it is a small pain. Once the SPARK lib is released on Alire, it should be replaced.
Changes to the API files and MXDR:
Improvements to Merc allow it to generate the API files for all of the core modules. All core modules now have auto-generated API files, with the exception of the Pub/Sub server.
File_Manager.mxdr now specifies the max file name and data size with the <> things.
Created mxdr spec for Log_Server
Generated api files now include Send_Message_Name procedures. This reduces boiler plate caused by memory allocation when sending messages and allows for greater message safety.
The send procedures have preconditions checking that the destination module exists in the destination domain and that the destination module may receive the message type being sent.
There are also weaker versions of the send procedures which don't check for all of these things. This is necessary for sending responses to messages when the destination module isn't known at compile time.
There's probably some more stuff but I don't have time to write it here.
This is all the changes I've made to CubedOS this summer. I was using individual commits, but I apparently have been working on an outdated local branch for the last month and don't know git well enough to deal with that in under a day. Also this refactor turned out to be very iterative and I think including the full git history would be mostly confusing to viewers.
Changes to project structure:
Changes to the message system:
Implementation Differences
Generic_Message_ManagerintoCubedOS.Message_Types. This resolves some circular dependency issues.Mutable_Message_Record.Message_Recordis now immutable. This was intended to aid the decoder functions while making it harder for module writers to screw up and produce invalid messages. It's usefulness for that application is limited though. It's still useful in a few select places so I decided to keep it.Added Debugging Feature
Domain and Module Addressing
name_resolverfile by creating aDomain_Metadataconstant which describes what modules are included in the domain, and the domain's number.Generic_Message_Manageris instantiated with a domain metadata object, supplying the message manager with more information to check safety with.Name_Resolveris now back to pre-domain syntax for assigning module IDs. Each module name is assigned a Module module ID instead of an address. If a module is in multiple domains, it's added in multiple domain metadata declarations.Safety Improvements
Universal_Message_Typerecord which identifies a message type uniquely across domains and modules. This enables greater safety.Module_Metadataobject containing this information which the module implements.Module_Mailboxobject which uniquely identifies the sending module.Skip_Mailbox_Initializationis called. This prevents messages from being lost at startup before mailbox size is determined. This is also enforced by SPARK.Waitfunction which blocks until the system is ready.Changes to Module Structure
Module_Mailboxobject to use the messaging system. They shouldn't use theFetchoperation anymore.Initprocedure which will be called from the Main procedure on startup which register's their mailbox.Changes to Transport Modules
Domain_Config.adbwhich CubedOS systems must implement. This function will inspect the message and then give it to a transport module.Handle_Receivedprocedure.Changes to Sample Programs
Changes to Core Modules
Changes to testing:
check_messaging_proof.adb. This is a manual test meant to verify that SPARK is providing appropriate feedback when attempting to read messages without proof that the message system is initialized.Changes to the CubedOS Library:
Changes to XDR lib
Max_TimeandMax_Time_Spanconstants to communicate the maximum supported time values in MXDR. This issue needs to be revisited in depth as I explain in the Merc repo https://github.com/cubesatlab/merc/issues/1Added Bounded Queue Implementation
Changes to the API files and MXDR:
<>things.Send_Message_Nameprocedures. This reduces boiler plate caused by memory allocation when sending messages and allows for greater message safety.There's probably some more stuff but I don't have time to write it here.