* skeletons, adding new constructs (arch_tcb, arch_fault)
* adjusting skeletons for ReserveIRQ + small change in haskell (ARM)
Changes in: spec/haskell/src/SEL4/Object/Interrupt/ARM.lhs:37:21
Due to "Defined but not used: ‘irq’"
* arch-splitting faults in skeletons (ARM)
* fix arch_tcb and asUser namespace issues in skeletons (ARM)
* checking in current generated files
tags: [VER-623][SELFOUR-413]
Hypervisor extensions add extra fault types which are entirely
arch-specific. While the concept of a VM fault exists on all platforms,
these faults are also arch-specific.
This change adds an ArchFault datatype and constructor to the generic
Faults and Failures, and moves VMFault into ArchFault for the ARM
platform.
NOTE: fault indices have changed (generic goes before arch) as per
the changes needed for SELFOUR-413, which is the seL4 C equivalent of
this commit.
* add arch faults and failures to SEL4.cabal
* introduce and handle IRQReserved
On ARM this does nothing, but on other platforms reserved IRQs are
actually used.
* split TCB into ArchTCB (userContext)
* changing ArchFault to make haskell-translator to work
tags: [VER-623][SELFOUR-413]
This reverts:
- a67b443ca5
"SELFOUR-242: update goal number based indentation in Fastpath_C"
- f704cf0404
"SELFOUR-242: invert bitfield scheduler and optimise fast path"
Verification confirmed functional correctness and refinement of the
system in this case. However, guarantees on thread scheduling and
fairness are not modeled in the current verification. Once this issue is
addressed, SELFOUR-242 will be re-examined.
Currently every image (heap?) is build in top of one (JUST ONE) ancestor image,
so there is no reason for any image-related test to depend on
more than 1 image-related test, granted no external things are being
build as a result of any dependency.
I'm keeping this separate as it changes a lot of whitespace that
SELFOUR-242 touches only indirectly by influencing the number of
subgoals.
A few small cleanups got thrown in.
* Reverse the level 2 of the bitmap scheduler to move the highest priority
threads' level 2 entries into the same cache line as the level 1.
* Use the bitfield scheduler to make the fast path a more common occurrence.
* Change possibleSwitchTo to not invoke scheduler when the fast path would not
invoke it either (using implicit assumptions about the current thread being
the highest priority schedulable thread)
These changes to the automatons are required by:
SELFOUR-242: invert bitfield scheduler and optimise fast path
Details:
When we enter the kernel, the domain time left (ksDomainTime) is never zero.
If we entered on a timer interrupt, we may decrement it to zero before the
scheduler runs. If we do so, we set the scheduler state to choose_new_thread.
When choosing a new thread, the scheduler switches to a new domain if the
present one is required, and sets the new domain time left from domain_list
(ksDomSchedule).
When entering the kernel on a non-interrupt event, we never touch the domain
time left, which trivially preserves the new constraints.
To prove these, we had to ban a transition from kernel entry to kernel being
preempted when handling an interrupt event in InfoFlow. This is fine, as by
design handling interrupts is not meant to be preempted by interrupts.
Analogous to the _UNIV versions, they are:
ccorres_symb_exec_r_rv_abstract: you know some property about the return
value you want to exploit
ccorres_symb_exec_r_known_rv: you know exactly how the return value
can be generated from the Haskell side (e.g. using from_bool, ucast)
As discussed in the past, the _UNIV versions can be dangerous as they
expect a trivial postcondition of the subsequent SIMPL statement.
The watch_kill_switch loop was pretty busy, adding a simple
timeout reduces CPU consumption.
The CPU consumption of run_tests.py is still higher than I'd expect
to just update a terminal, but I don't know where to investigate
further.
Figured out how to pass the necessary assumptions about the region
being zeroed through the createNewObjects loop and resolve at
invokeUntyped_Retype. Still WIP.
This is a work-in-progress tool for producing simp rules for functions on a
record that don't look at all the record's state. For instance, given a record
with fields a, b, c, and a function "f x = a x + b x", the tool should
automatically prove that "f (c_update f x) = f x".
At version 4.1.0, the Python psutil package changed the way it reports
CPU times for processes. This commit ensures that regression tests are
compatible with both old and new psutil APIs.
Adding optional tracing makes the bug clear; the subgoals of the
rules are attacked in the opposite order, so congruence-style rules
which introduce extra assumptions would have the (schematic)
assumptions unified out of order. Fixed.
WPC was written somewhat conservatively to raise exceptions if
something surprising happens. One surprising thing is multiple
higher-order resolution candidates, caused by such things as
a previous precondition of the form "?P x y None None". This isn't
really a problem, so a slight tweak should suppress the exception.
To finish the proof of refinement to C, the specification for checkPrio
needed strengthening: the checkPrio spec now takes a machine word
argument. In the spec, priorities are still stored as 8-bit quantities,
however. Once the spec was strenthened, it was possible to remove some
redundant checks and mask operations from the C code.
A thread's maximum controlled priority (MCP) determines the maximum
thread priority or MCP it can assign to another thread (or itself).
Also includes fixes to specs and invariants, and initial progress
towards C refinement.
A thread's maximum controlled priority (MCP) determines the maximum
thread priority or MCP it can assign to another thread (or itself).
Miki Tanaka
Rafal Kolanski
Xin,Gao
Joel Beeren
Alejandro Gomez-Londono
Ramana Kumar
Thomas Sewell
Matthew Brecknell
Sophie Taylor