Repository navigation
test(m2-10): integrated campaign, coverage, and two scheduler/sanitizer fixes - #38
Merged
Merged
Conversation
…unner
- The COMBINED scenario group meets several mechanisms at section
boundaries, with ISR and tick placement left to the explorer and the
bridge:
- a suspended, canceled and resumed message queue receiver against an
ISR send;
- an inheriting owner's priority change against an event wait's timeout
and an ISR set;
- a timed take against a give and destroy at the same ticks;
- one thread bound to a message queue and to event flags;
- an ISR-context timer feeding a queue a work handler reads while the
thread flushes and stops it;
- an ISR cancel racing a delayed item's expiry.
- native-coverage preset: GCC with --coverage at -O0. The native port
dumps the gcov counters before _exit(), which skips the exit-time
flush.
- tools/coverage/report.py: kernel statement and branch coverage from
gcov or llvm-cov gcov, with file exclusions and their reasons.
- tools/model/campaign.py: runs the bridge over runners and seeds plus
the timer regressions and writes a JSON summary with the build
identities.
Signed-off-by: teo1747 <motsoujunior17@gmail.com>
…once embk_sched_prio_changed() set reschedule_pending only when the running thread's own effective priority fell below a ready thread. When another thread raised a ready thread above the caller with emb_thread_set_priority(), nothing marked the reschedule, and the caller kept running past its preemption point until its next block or yield. The M2-10 combined campaign found it: in release builds, where the scenario's owner-death policy lets the run continue, a raised owner did not run before the raising thread's next wait. The hook now marks the reschedule when a ready thread other than the running one rises above it. The new case sched_raising_a_ready_thread_above_the_caller_preempts fails on the old kernel (marks 1, 3, 2) and passes now. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
…izer
Clang's AddressSanitizer on Mach-O pads globals in custom sections with
redzones, so walking the test or init table read the padding as
entries. Every conformance suite aborted with a global-buffer-overflow
in the runner, and native-asan could not run on macOS. ELF builds leave
section globals alone, which is why CI passed.
Table entries now carry EMB_TABLE_ENTRY_ATTR: no_sanitize("address")
under Clang with AddressSanitizer, empty everywhere else. native-asan
passes 20/20 locally and the tiny ASan build 17/17.
Signed-off-by: teo1747 <motsoujunior17@gmail.com>
Signed-off-by: teo1747 <motsoujunior17@gmail.com>
The previous fix marked the reschedule in the scheduler's priority hook, which the inheritance recomputation calls. A build without mutexes, such as the tiny footprint configuration, sets the effective priority directly and never reaches that hook, so sched_raising_a_ready_thread_above_the_caller_preempts still failed on avr-uno-t1. emb_thread_set_priority() now checks the raised thread against the running one itself. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
- tools/model/evidence/m2-10/: the campaign summaries for native gcc, clang, periodic, release and tiny (seeds 1-10, --runs 40, plus the timer regressions): 158,800 runs, no divergence, clean tree at f563ef5. Also the kernel coverage (91.4% of lines, 72.5% of branches, nothing excluded) and the requirement-matrix summary over all 21 configurations. - docs/engineering/m2-10-campaign.md reports the combined scenarios, the two defects the campaign found (the missing preemption on a priority raise and the macOS AddressSanitizer table padding), the sanitizer results, the lowest-covered files, and the implemented requirements verified by analysis rather than by a case. - CI builds native-coverage, publishes the report and runs the report tool's tests. The sanitizer and coverage configurations join the evidence catalogue. - msgq_small_counts_refuse_a_capacity_above_255 gives KRN-IPC-021 an executed case. - The checklist's two campaign items, STATUS and the changelog are updated. Signed-off-by: teo1747 <motsoujunior17@gmail.com>
5 of 6 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacked on #37. This completes the first two M2-10/M2-11 checklist items: the combined campaign, and the misuse, property, sanitizer and coverage results.
Problem and result
M2-10 asks for mechanisms combined at section boundaries under adversarial interrupt and tick placement, plus sanitizer runs and statement and branch coverage with real case identity. Disclosed gaps are acceptable; unexplained failures are not.
COMBINEDmodel group has six scenarios. Each pairs a primitive with cancel, suspend, destroy, a priority change, bindings, or timer and work callbacks.emb_thread_set_priority()did not preempt: the caller kept running until its next block or yield. The new casesched_raising_a_ready_thread_above_the_caller_preemptsfails on the old kernel and passes on every target.native-asanpasses 20/20 locally.native-coveragepreset plustools/coverage/report.py. The native port now dumps gcov counters before_exit(), which otherwise skips the flush. CI builds the preset, publishes the report and tests the report tool.tools/model/campaign.pyruns the whole catalogue over runners and seeds, plus the timer regressions, and writes summaries with build identities.tools/model/evidence/m2-10/; the report isdocs/engineering/m2-10-campaign.md.Validation
Campaign. Seeds 1–10,
--runs 40, plus the regressions, on a clean tree atf563ef5:158,800 runs, no divergence.
Every local configuration passes.
Coverage. 91.4% of 2,900 kernel lines and 72.5% of 1,472 branches, over all 18 base-build kernel files; nothing is excluded. The report explains the lowest-covered files.
Requirement matrix. No failed case in any configuration. 127 of 377 requirements have a passing executed case.
Model. 122 model tests pass.
Footprint. T1 is unchanged (4,056 / 39 / 32).
Lint and docs. Docs tests OK; the local docs build shows the same nine shim warnings; banned-pattern check 0 findings; clang-format clean.
Not run. Hardware-in-the-loop and physical timing (no board), and the EmbCC native flow.
Review checklist
Signed-off-bytrailer (git commit -s); DCO is separate from cryptographic signing.