Skip to content

Book v1.4 — Bare-Metal Ada on the ESP32-S3

Choose a tag to compare

View all tags
@github-actions github-actions released this 28 Jul 19:41
· 58 commits to main since this release
v1.4
5a3d3e0
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

Capability + correctness release. The whole runtime now builds and runs with assertions enabled (BUILD=Assert, RTS-wide -gnata) on all three profiles — and doing so flushed out three latent kernel bugs — and the full profile can place task stacks in external PSRAM. All fixes hardware-verified on the ESP32-S3-Touch-LCD-7.

Runtime fixes

  • Ghost ready-queue invariant + cycle-safe queue walks, plus four more dev-only invariants (alarm queue, systimer, poke, cross-cancel) — the assertion net that caught what follows. (#190, #191)
  • Cross-core served-entry self-deadlock — the entry-serving path now masks across its lock hold. (#192)
  • Stale kernel base priority — a task activated while its activator held a default-ceiling lock kept kernel base 255 for life; Set_Priority now reconciles it (the creation-time alternative deadlocks the ACATS-mandated activation handshake). (#193)
  • SMP-unsound Current_Priority postcondition removed — it re-read scheduler state another core mutates concurrently; no sound contract can express it. (#194)
  • PSRAM task stacks — the vector SP sanity guard now accepts the PSRAM d-bus window, making full-profile task stacks in PSRAM (__gnat_task_stack_alloc / HEAP_PSRAM) a working, verified configuration: 1.45M checksum-verified deep recursions on a PSRAM stack, 300k protected-entry rendezvous, and a full GUI application running its task set from a PSRAM arena. (#195)

Book

  • BUILD=Assert documented as the runtime's torture test; PSRAM task stacks, the vector sanity net, and the stale-registers-at-a-park decoding trap. (#196)
  • Stale claims fixed: PSRAM is DMA-reachable (through the DCache, cache-line aligned), GDMA Wait blocks on an interrupt, Send_Socket is a partial send. (#197)
  • Per-task CPU accounting (System.BB.Execution_Time), the real SMP affinity semantics (unpinned = the creator's core, for life), and the watchpoint-redzone constraint on stack-painting monitors. (#198)
  • References to the private examples collection reworded so the public book stands alone. (#199)

Runtime packs regenerated where RTS source changed.

The attached PDF is the full book (342 pages) built at this tag.

What's Changed

  • rts: ghost ready-queue invariant + cycle-safe queue walks by @rowsail in #190
  • rts: four more dev-only invariants (alarm queue, systimer, poke, cross-cancel) by @rowsail in #191
  • rts: fix cross-core served-entry self-deadlock (mask the lock hold) by @rowsail in #192
  • rts: reconcile a task's stale kernel base priority in Set_Priority by @rowsail in #193
  • rts: drop the unsound Current_Priority postcondition (SMP race) by @rowsail in #194
  • rts: accept PSRAM stacks in the vector SP sanity guard by @rowsail in #195
  • book: document PSRAM task stacks, the vector sanity net, and BUILD=Assert by @rowsail in #196
  • book: fix stale claims (PSRAM DMA, GDMA Wait, Send_Socket contract) by @rowsail in #197
  • book: per-task CPU accounting, real affinity semantics, the redzone trap by @rowsail in #198
  • book: stop pointing readers at the private examples collection by @rowsail in #199

Full Changelog: v1.3.2...v1.4

Contributors

rowsail
Assets 3
Loading