Do not provide SIMULATION ON by default. This avoids
surprising compilation failures on platforms that do not support
simulation settings.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The Cogent project is no longer actively developed on top of seL4, and
the upstream build has broken.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The tests look for "B: Exiting" on the console to confirm that the test
has passed. Try and let the other component complete before printing the
last message so that it doesn't get interleaved due to preemptive
scheduling.
Signed-off-by: Kent McLeod <kent@kry10.com>
The trigger action sends repository_dispatch events to all
main test repositories of the manifests this repo is part of.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Setting LibPicotcp=ON in a settings.cmake will remove picotcp
compilation errors when this app configuration is built.
Signed-off-by: Kent McLeod <kent@kry10.com>
With the latest changes to the DMA allocation in libsel4camkes, the
default DMA pool for each component is now uncached, hence we also
update the sources to use uncached memory.
Following the latest changes to the DMA allocation in libsel4camkes
where it is now aware of cached DMA allocations, this commit changes the
DMA allocation calls to allocate uncached memory as the default pool is
mapped uncached.
This allows the simulation settings to distinguish between ia32 and x86_
64 when setting for simulation.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This allows the simulation settings to distinguish between ia32 and x86_
64 when setting for simulation.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Consider 3 threads with budget and period setting as T_1(90 / 200),
T_2(60 / 250), and T_3(10 / 300), sorted in descending order of
priority. The sum of CPU utilization is 72.3% thus meet the
schedulability requirement of Rate-monotonic scheduling, which
means the lower priority thread T_3 will always have its chance to
run in any of its periods. The example demonstrates this working.
- Add a socket for starting and stopping and reporting utilization
information gathering
- Add BenchUtiliz component for performing measurements and also tracing
support.
These async interfaces use virtqueues to batch multiple receive and send
operations together. This change applies to both the TCP connections and
UDP socket. The socket functionality was moved into separate files also.
Since this was originally written, the syntax of theorem statements
changed, a conversion that breaks the proofs was added to the
default simpset, and and some of the functionality inlined here
was upstreamed to HOL4 libraries.
This is intended to run on CakeML version 6f71ec748.
Signed-off-by: Johannes Åman Pohjola <johannes.amanpohjola@data61.csiro.au>
Gerwin Klein