Gerwin Klein
Gerwin Klein
In this run: https://github.com/seL4/util_libs/actions/runs/4920068732/jobs/8789972531?pr=156#step:4:3957 we're getting: ``` Tue, 09 May 2023 02:21:49 GMT Test SCHED0010 passed Tue, 09 May 2023 02:21:49 GMT Tue, 09 May 2023 02:21:49 GMT Tue, 09...
(Imported form https://sel4.atlassian.net/browse/SELFOUR-2377) simulation sel4test builds don't run any MCS configurations. Historically this was because of many of the tests are time sensitive and don't handle Qemu's emulation of time...
`skylake` produces output such as ``` IOMMU: DMA write page fault from 0xa0 (bus: 0x0/dev: 0x14/fun: 0x0) on address 0x0:dc2f9000 with reason code 0x5 ``` interleaved with normal test output,...
We introduced a MIN_BUDGET test in https://github.com/seL4/sel4test/commit/b572953ffd41949c15afdfa611de140377dca59f which succeeded for everything tested at the time, but since then the TK1 board has come online. The TK1 board is defined with...
- `lockTLBEntry` uses the global `tlbLockCount` as input without checking bounds. This is fine, because the function is called at most 2 times on unicore platforms, but this is only...
This is work by @kent-mcleod, with an additional commit on top from myself with verification tweaks for this new API. For design rationale and background on the API in this...
`xxd` is needed in `elfloader-tool` in some configs. See also https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles/pull/70
As discovered in #163, the docsite build is breaking with the default versions of ruby and bundler on Ubuntu 22.04. We should update the dependencies such that they are more...
seL4/seL4#896 changes IOAPIC-related decoding slightly and requires a few new small invariants on the Haskell level. Test with: seL4/seL4#896
Inspired by discussions on the fastpath PR and MM discussions, a minor addition to the CRefine notes in `docs/` on how to debug that `False`-in-final-goal-after-`vcg` problem.