This PR ensures that the sDDF is in line with what is described in the design document, along with a few extra usability improvements and minor fixes. Changes include:
Ensuring all virtual addresses configured with microkit are mapped in using setvaddr
Removing an unnecessary channel from the timer to the tx virtualiser
Fixing an incorrect macro that set the rx virtualiser's queue size to the client's size rather than the copier's size
Ensuring cache invalidates are cache line aligned, fixing the ROUND_UP macro which is used to calculate this
Updating the queue data structure to ensure the consumer_signalled flag is on the same cache line as the head and tail pointers, and changing it's type to uint64_t
Removing any array accesses using the queue head and tail pointers directly, instead the descriptor array is only accessed modulo the queue size. Queue size is also removed from the shared queue data structure and instead stored in the local queue handle data structure. Therefore, all queue operations are now performed on the queue handle rather than the queues individually, so there are two sets of queue functions for each operation (one for active and one for free)
Fix the shared memory operations in idle.c and utilisation_socket.c so that reads and writes to their shared memory are atomic. Remove incorrect overflow handling code which handled uint64_t overflows and was never invoked (even if it were to have been invoked, it was incorrect)
Ensure microkit_notify_delayed is used where possible
Add Spin promella models to the echo_server example which were used to verify the signalling protocol
Stop the benchmark and idle PDs from crashing when built in debug mode
Add informative fault information to the parent benchmark PD which details how the child process faulted
This PR ensures that the sDDF is in line with what is described in the design document, along with a few extra usability improvements and minor fixes. Changes include:
microkit
are mapped in usingsetvaddr
ROUND_UP
macro which is used to calculate thisconsumer_signalled
flag is on the same cache line as the head and tail pointers, and changing it's type touint64_t
uint64_t
overflows and was never invoked (even if it were to have been invoked, it was incorrect)microkit_notify_delayed
is used where possibleecho_server
example which were used to verify the signalling protocol