edu-freertos-c/lab-rv32i-freertos-c-static-allocation
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

feat: publish FreeRTOS C FC11 card

Browse Source
This commit is contained in:
M. Pabiszczak
2026-07-19 16:36:03 +02:00
commit 0464bf759a
196 changed files with 61224 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
web/figures/a1-context.puml
+19
View File
@@ -0,0 +1,19 @@
@startuml
skinparam backgroundColor transparent
skinparam shadowing false
skinparam defaultFontName Monospace
skinparam defaultFontSize 12
skinparam rectangleBorderColor #2c7794
skinparam rectangleBackgroundColor #edf6fa
title A1 CONTEXT — who owns task, queue and timer storage
rectangle "01 Application\nmain + verifier" as app
rectangle "02 Dynamic branch\nxTaskCreate\nxQueueCreate\nxTimerCreate" as dyn
rectangle "03 Static branch\nxTaskCreateStatic\nxQueueCreateStatic\nxTimerCreateStatic" as stat
rectangle "04 FreeRTOS kernel\nTCB · queue · timer daemon" as kernel
rectangle "05 Hazard3 RAM\nucHeap + named buffers" as ram
app --> dyn : asks kernel to allocate
app --> stat : supplies persistent storage
dyn --> kernel
stat --> kernel
kernel --> ram
@enduml
web/figures/a1-context.svg
+41
View File
@@ -0,0 +1,41 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?><svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" contentScriptType="application/ecmascript" contentStyleType="text/css" height="478px" preserveAspectRatio="none" style="width:369px;height:478px;" version="1.1" viewBox="0 0 369 478" width="369px" zoomAndPan="magnify"><defs/><g><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="315" x="31" y="12.8281">A1 CONTEXT — who owns task, queue and timer storage</text><!--MD5=[4541fb81c80c07473fe4b07432ef0971]
entity app--><rect fill="#EDF6FA" height="52.6882" style="stroke: #2C7794; stroke-width: 1.5;" width="101" x="102.5" y="23.9041"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="79" x="112.5" y="46.7322">01 Application</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="81" x="112.5" y="63.0763">main + verifier</text><!--MD5=[2fdd58fa1f9dca7f678b1591ba5c253a]
entity dyn--><rect fill="#EDF6FA" height="85.3765" style="stroke: #2C7794; stroke-width: 1.5;" width="128" x="6" y="154.5941"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="108" x="16" y="177.4222">02 Dynamic branch</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="70" x="16" y="193.7663">xTaskCreate</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="81" x="16" y="210.1104">xQueueCreate</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="77" x="16" y="226.4545">xTimerCreate</text><!--MD5=[299d1c4a2ba6184a4b2319b3d939ce68]
entity stat--><rect fill="#EDF6FA" height="85.3765" style="stroke: #2C7794; stroke-width: 1.5;" width="132" x="169" y="154.5941"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="90" x="179" y="177.4222">03 Static branch</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="101" x="179" y="193.7663">xTaskCreateStatic</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="112" x="179" y="210.1104">xQueueCreateStatic</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="108" x="179" y="226.4545">xTimerCreateStatic</text><!--MD5=[5427960f0a0d6e728427509f19a12a87]
entity kernel--><rect fill="#EDF6FA" height="52.6882" style="stroke: #2C7794; stroke-width: 1.5;" width="175" x="64.5" y="300.9641"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="110" x="74.5" y="323.7922">04 FreeRTOS kernel</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="155" x="74.5" y="340.1363">TCB · queue · timer daemon</text><!--MD5=[86bcb769366fd3cf48170f656eee3c0e]
entity ram--><rect fill="#EDF6FA" height="52.6882" style="stroke: #2C7794; stroke-width: 1.5;" width="158" x="73" y="414.6541"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="94" x="83" y="437.4822">05 Hazard3 RAM</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="138" x="83" y="453.8263">ucHeap + named buffers</text><!--MD5=[844223e7c20978ac4b81c22d2d6ee8bd]
link app to dyn--><path d="M102.02,70.8041 C86.71,79.3541 71.68,91.0641 63,106.5941 C56.06,119.0041 54.94,133.9341 56.38,148.0141 " fill="none" id="app-&gt;dyn" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="57.02,152.9141,59.8293,143.4744,56.377,147.9556,51.8958,144.5033,57.02,152.9141" style="stroke: #A80036; stroke-width: 1.0;"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="124" x="64" y="120.4222">asks kernel to allocate</text><!--MD5=[e0f7f866026d3174b64552b149f8696b]
link app to stat--><path d="M175.8,76.9341 C183.13,85.9341 190.92,96.3541 197,106.5941 C204.79,119.6941 211.8,134.6841 217.62,148.6141 " fill="none" id="app-&gt;stat" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="219.47,153.1141,219.7787,143.2701,217.5835,148.4837,212.37,146.2885,219.47,153.1141" style="stroke: #A80036; stroke-width: 1.0;"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="151" x="206.9" y="120.4222">supplies persistent storage</text><!--MD5=[95003ff17088984a22052575ee8d8137]
link dyn to kernel--><path d="M96.85,240.2041 C108.35,258.1541 121.54,278.7541 132.14,295.2941 " fill="none" id="dyn-&gt;kernel" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="134.81,299.4741,133.3229,289.7382,132.1127,295.2641,126.5868,294.0538,134.81,299.4741" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[88142749908d9e422477f0519a59cdc1]
link stat to kernel--><path d="M207.82,240.2041 C196.18,258.1541 182.83,278.7541 172.11,295.2941 " fill="none" id="stat-&gt;kernel" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="169.4,299.4741,177.6574,294.1061,172.1239,295.2812,170.9488,289.7478,169.4,299.4741" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[f7b1c250898a6b689ea9b5bb053ebce9]
link kernel to ram--><path d="M152,353.9341 C152,370.1141 152,391.1241 152,408.3441 " fill="none" id="kernel-&gt;ram" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="152,412.9841,156,403.9841,152,407.9841,148,403.9841,152,412.9841" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[c715fc12bd8ef68b76af2fdf54c0f1d5]
@startuml
skinparam backgroundColor transparent
skinparam shadowing false
skinparam defaultFontName Monospace
skinparam defaultFontSize 12
skinparam rectangleBorderColor #2c7794
skinparam rectangleBackgroundColor #edf6fa
title A1 CONTEXT — who owns task, queue and timer storage
rectangle "01 Application\nmain + verifier" as app
rectangle "02 Dynamic branch\nxTaskCreate\nxQueueCreate\nxTimerCreate" as dyn
rectangle "03 Static branch\nxTaskCreateStatic\nxQueueCreateStatic\nxTimerCreateStatic" as stat
rectangle "04 FreeRTOS kernel\nTCB · queue · timer daemon" as kernel
rectangle "05 Hazard3 RAM\nucHeap + named buffers" as ram
app - -> dyn : asks kernel to allocate
app - -> stat : supplies persistent storage
dyn - -> kernel
stat - -> kernel
kernel - -> ram
@enduml
PlantUML version 1.2020.02(Sun Mar 01 11:22:07 CET 2020)
(GPL source distribution)
Java Runtime: OpenJDK Runtime Environment
JVM: OpenJDK 64-Bit Server VM
Java Version: 25.0.4-ea+4-1-Debian
Operating System: Linux
Default Encoding: UTF-8
Language: en
Country: null
--></g></svg>
Side by Side

After

Width:  |  Height:  |  Size: 6.8 KiB

web/figures/a2-structure.puml
+25
View File
@@ -0,0 +1,25 @@
@startuml
skinparam backgroundColor transparent
skinparam shadowing false
skinparam defaultFontName Monospace
skinparam defaultFontSize 11
skinparam rectangleBorderColor #2c7794
skinparam rectangleBackgroundColor #edf6fa
title A2 STRUCTURE — equal kernel objects, different storage policy
rectangle "01 Dynamic task\nTCB + stack in ucHeap" as dt
rectangle "02 Static task\nStaticTask_t + StackType_t[]" as st
rectangle "03 Dynamic queue\nobject + item buffer in ucHeap" as dq
rectangle "04 Static queue\nStaticQueue_t + uint8_t[]" as sq
rectangle "05 Dynamic timer\ntimer object in ucHeap" as dm
rectangle "06 Static timer\nStaticTimer_t" as sm
rectangle "07 Static kernel services\nIdle TCB/stack\nTimer daemon TCB/stack" as svc
dt -[hidden]right- st
dq -[hidden]right- sq
dm -[hidden]right- sm
dt -down-> dq : same message 0xCAFE
st -down-> sq : same message 0xCAFE
dq -down-> dm : one-shot callback
sq -down-> sm : one-shot callback
svc ..> dm
svc ..> sm
@enduml
web/figures/a2-structure.svg
+53
View File
@@ -0,0 +1,53 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?><svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" contentScriptType="application/ecmascript" contentStyleType="text/css" height="350px" preserveAspectRatio="none" style="width:594px;height:350px;" version="1.1" viewBox="0 0 594 350" width="594px" zoomAndPan="magnify"><defs/><g><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="328" x="136.5" y="11.7589">A2 STRUCTURE — equal kernel objects, different storage policy</text><!--MD5=[3f813737a27eb5cca819d156ac1ac98b]
entity dt--><rect fill="#EDF6FA" height="49.9638" style="stroke: #2C7794; stroke-width: 1.5;" width="133" x="178.5" y="23.1119"/><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="84" x="188.5" y="44.8708">01 Dynamic task</text><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="113" x="188.5" y="59.8527">TCB + stack in ucHeap</text><!--MD5=[5d4b2633e4791513268a2604d42d888f]
entity st--><rect fill="#EDF6FA" height="49.9638" style="stroke: #2C7794; stroke-width: 1.5;" width="161" x="371.5" y="23.1119"/><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="67" x="381.5" y="44.8708">02 Static task</text><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="141" x="381.5" y="59.8527">StaticTask_t + StackType_t[]</text><!--MD5=[008c4d17aac760e260395f8e0c37c22a]
entity dq--><rect fill="#EDF6FA" height="49.9638" style="stroke: #2C7794; stroke-width: 1.5;" width="178" x="6" y="156.5619"/><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="96" x="16" y="178.3208">03 Dynamic queue</text><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="158" x="16" y="193.3027">object + item buffer in ucHeap</text><!--MD5=[559b856ebbf6540c39b50745da7961f2]
entity sq--><rect fill="#EDF6FA" height="49.9638" style="stroke: #2C7794; stroke-width: 1.5;" width="148" x="403" y="156.5619"/><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="79" x="413" y="178.3208">04 Static queue</text><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="128" x="413" y="193.3027">StaticQueue_t + uint8_t[]</text><!--MD5=[158b8a3ce0eb6bdeb9584db5e4540d4f]
entity dm--><rect fill="#EDF6FA" height="49.9638" style="stroke: #2C7794; stroke-width: 1.5;" width="138" x="148" y="290.0219"/><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="91" x="158" y="311.7808">05 Dynamic timer</text><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="118" x="158" y="326.7627">timer object in ucHeap</text><!--MD5=[31b50539c062e48f418cd0b43b66a14f]
entity sm--><rect fill="#EDF6FA" height="49.9638" style="stroke: #2C7794; stroke-width: 1.5;" width="94" x="321" y="290.0219"/><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="74" x="331" y="311.7808">06 Static timer</text><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="67" x="331" y="326.7627">StaticTimer_t</text><!--MD5=[253793ac12dc71b5b3661728e8dc2147]
entity svc--><rect fill="#EDF6FA" height="64.9457" style="stroke: #2C7794; stroke-width: 1.5;" width="149" x="218.5" y="149.0719"/><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="123" x="228.5" y="170.8308">07 Static kernel services</text><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="73" x="228.5" y="185.8127">Idle TCB/stack</text><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="129" x="228.5" y="200.7946">Timer daemon TCB/stack</text><!--MD5=[c443e4b075ff3fce78d00ed6a2632c8e]
link dt to st--><!--MD5=[6be6bd5e6654fbf03a74c7794a8b1ee8]
link dq to sq--><!--MD5=[4acaab06e73e6cd463470f1aa16c5f6c]
link dm to sm--><!--MD5=[f3553b6e97ea8e5802b4e5e32830efc1]
link dt to dq--><path d="M217.14,73.5119 C191.77,95.7319 154.31,128.5619 127.58,152.0019 " fill="none" id="dt-&gt;dq" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="123.85,155.2619,133.2517,152.328,127.6067,151.9623,127.9724,146.3173,123.85,155.2619" style="stroke: #A80036; stroke-width: 1.0;"/><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="116" x="179.98" y="115.8308">same message 0xCAFE</text><!--MD5=[394fd7d603290abaaea335171f5bd6de]
link st to sq--><path d="M456.64,73.5119 C460.75,95.0919 466.75,126.6619 471.18,149.9319 " fill="none" id="st-&gt;sq" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="472.1,154.7719,474.3594,145.1857,471.1717,149.8588,466.4985,146.671,472.1,154.7719" style="stroke: #A80036; stroke-width: 1.0;"/><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="116" x="466.25" y="115.8308">same message 0xCAFE</text><!--MD5=[e2ee8be0d8a5fab4f61e8b60cd7d4f8a]
link dq to dm--><path d="M109.41,206.9419 C119.45,222.9219 133.73,243.7719 149,260.0219 C157.53,269.0919 167.63,277.9319 177.4,285.7419 " fill="none" id="dq-&gt;dm" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="181.29,288.7919,176.6872,280.0847,177.3594,285.7015,171.7426,286.3737,181.29,288.7919" style="stroke: #A80036; stroke-width: 1.0;"/><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="91" x="150" y="256.7808">one-shot callback</text><!--MD5=[7af305701224b1d55b1776e9d524f9d0]
link sq to sm--><path d="M456.75,206.9619 C438.48,229.0019 411.55,261.4719 392.16,284.8619 " fill="none" id="sq-&gt;sm" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="389.1,288.5519,397.9233,284.176,392.2911,284.7026,391.7645,279.0703,389.1,288.5519" style="stroke: #A80036; stroke-width: 1.0;"/><text fill="#000000" font-family="Monospace" font-size="11" lengthAdjust="spacingAndGlyphs" textLength="91" x="426.77" y="256.7808">one-shot callback</text><!--MD5=[d31579fe64ed4afdfe5e7cb18479b6e7]
link svc to dm--><path d="M274.6,214.3619 C262.26,235.7119 246.12,263.6219 234.07,284.4719 " fill="none" id="svc-&gt;dm" style="stroke: #A80036; stroke-width: 1.0; stroke-dasharray: 7.0,7.0;"/><polygon fill="#A80036" points="231.7,288.5719,239.665,282.7789,234.2007,284.2421,232.7374,278.7778,231.7,288.5719" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[a02bf47346101d362cc0b349394bde43]
link svc to sm--><path d="M311.16,214.3619 C323.33,235.7119 339.26,263.6219 351.15,284.4719 " fill="none" id="svc-&gt;sm" style="stroke: #A80036; stroke-width: 1.0; stroke-dasharray: 7.0,7.0;"/><polygon fill="#A80036" points="353.49,288.5719,352.5151,278.7714,351.017,284.2263,345.5621,282.7282,353.49,288.5719" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[79c4140bd63de98bcd572d35f61abe00]
@startuml
skinparam backgroundColor transparent
skinparam shadowing false
skinparam defaultFontName Monospace
skinparam defaultFontSize 11
skinparam rectangleBorderColor #2c7794
skinparam rectangleBackgroundColor #edf6fa
title A2 STRUCTURE — equal kernel objects, different storage policy
rectangle "01 Dynamic task\nTCB + stack in ucHeap" as dt
rectangle "02 Static task\nStaticTask_t + StackType_t[]" as st
rectangle "03 Dynamic queue\nobject + item buffer in ucHeap" as dq
rectangle "04 Static queue\nStaticQueue_t + uint8_t[]" as sq
rectangle "05 Dynamic timer\ntimer object in ucHeap" as dm
rectangle "06 Static timer\nStaticTimer_t" as sm
rectangle "07 Static kernel services\nIdle TCB/stack\nTimer daemon TCB/stack" as svc
dt -[hidden]right- st
dq -[hidden]right- sq
dm -[hidden]right- sm
dt -down-> dq : same message 0xCAFE
st -down-> sq : same message 0xCAFE
dq -down-> dm : one-shot callback
sq -down-> sm : one-shot callback
svc ..> dm
svc ..> sm
@enduml
PlantUML version 1.2020.02(Sun Mar 01 11:22:07 CET 2020)
(GPL source distribution)
Java Runtime: OpenJDK Runtime Environment
JVM: OpenJDK 64-Bit Server VM
Java Version: 25.0.4-ea+4-1-Debian
Operating System: Linux
Default Encoding: UTF-8
Language: en
Country: null
--></g></svg>
Side by Side

After

Width:  |  Height:  |  Size: 8.4 KiB

web/figures/a4-application.puml
+18
View File
@@ -0,0 +1,18 @@
@startuml
skinparam backgroundColor transparent
skinparam shadowing false
skinparam defaultFontName Monospace
skinparam defaultFontSize 12
skinparam rectangleBorderColor #2c7794
skinparam rectangleBackgroundColor #edf6fa
title A4 APPLICATION — behavior parity is part of the proof
rectangle "01 dynamic worker\nreceive 0xCAFE\nstart dynamic timer" as dyn
rectangle "02 static worker\nreceive 0xCAFE\nstart static timer" as stat
rectangle "03 timer daemon\ndynamic callback = 1\nstatic callback = 1" as daemon
rectangle "04 verifier\nmessage parity\ncallback parity\ndistinct stacks" as verify
dyn --> daemon
stat --> daemon
dyn --> verify
stat --> verify
daemon --> verify
@enduml
web/figures/a4-application.svg
+39
View File
@@ -0,0 +1,39 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?><svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" contentScriptType="application/ecmascript" contentStyleType="text/css" height="378px" preserveAspectRatio="none" style="width:324px;height:378px;" version="1.1" viewBox="0 0 324 378" width="324px" zoomAndPan="magnify"><defs/><g><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="303" x="9.5" y="12.8281">A4 APPLICATION — behavior parity is part of the proof</text><!--MD5=[2fdd58fa1f9dca7f678b1591ba5c253a]
entity dyn--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="129" x="6" y="23.9041"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="106" x="16" y="46.7322">01 dynamic worker</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="86" x="16" y="63.0763">receive 0xCAFE</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="109" x="16" y="79.4204">start dynamic timer</text><!--MD5=[299d1c4a2ba6184a4b2319b3d939ce68]
entity stat--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="112" x="191.5" y="23.9041"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="89" x="201.5" y="46.7322">02 static worker</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="86" x="201.5" y="63.0763">receive 0xCAFE</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="92" x="201.5" y="79.4204">start static timer</text><!--MD5=[995a46705506099b563611b182911a66]
entity daemon--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="135" x="81" y="152.9341"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="96" x="91" y="175.7622">03 timer daemon</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="115" x="91" y="192.1063">dynamic callback = 1</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="98" x="91" y="208.4504">static callback = 1</text><!--MD5=[43277b5e5915b8aad291fb6c6bd0e270]
entity verify--><rect fill="#EDF6FA" height="85.3765" style="stroke: #2C7794; stroke-width: 1.5;" width="106" x="95.5" y="281.9641"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="57" x="105.5" y="304.7922">04 verifier</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="86" x="105.5" y="321.1363">message parity</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="80" x="105.5" y="337.4804">callback parity</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="78" x="105.5" y="353.8245">distinct stacks</text><!--MD5=[bea346f714fb01cb80d7f2e7dbd64f2b]
link dyn to daemon--><path d="M91.2,93.1241 C101.42,109.7841 113.82,129.9741 124.46,147.3041 " fill="none" id="dyn-&gt;daemon" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="126.91,151.2941,125.5852,141.5348,124.2831,147.0397,118.7782,145.7377,126.91,151.2941" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[455cce1656bdd5dce2f89c06f912f1d1]
link stat to daemon--><path d="M221.23,93.1241 C208.14,109.9241 192.25,130.3141 178.66,147.7541 " fill="none" id="stat-&gt;daemon" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="175.82,151.3941,184.5064,146.7522,178.8927,147.4497,178.1952,141.836,175.82,151.3941" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[55f9ed2204fe7b44e8df8666194ec3de]
link dyn to verify--><path d="M61.71,93.2441 C54.63,126.9441 48.13,179.6141 63.5,221.9641 C70.76,241.9641 83.85,260.7741 97.63,276.6541 " fill="none" id="dyn-&gt;verify" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="100.92,280.3541,97.9304,270.97,97.5982,276.6171,91.9511,276.2849,100.92,280.3541" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[0b779b9021da6d81f69dcc0e6137211d]
link stat to verify--><path d="M250.36,93.1741 C251.93,127.0441 250.78,180.0741 233.5,221.9641 C225.31,241.8241 211.8,260.7241 197.92,276.7141 " fill="none" id="stat-&gt;verify" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="194.62,280.4541,203.5812,276.3679,197.9347,276.7108,197.5918,271.0643,194.62,280.4541" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[97dcfe194a7fdfb828de87be35f0eec1]
link daemon to verify--><path d="M148.5,222.2241 C148.5,238.2441 148.5,257.6841 148.5,275.2341 " fill="none" id="daemon-&gt;verify" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="148.5,280.0941,152.5,271.0941,148.5,275.0941,144.5,271.0941,148.5,280.0941" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[a8a1b31c45c5f222072643cce2cd8c96]
@startuml
skinparam backgroundColor transparent
skinparam shadowing false
skinparam defaultFontName Monospace
skinparam defaultFontSize 12
skinparam rectangleBorderColor #2c7794
skinparam rectangleBackgroundColor #edf6fa
title A4 APPLICATION — behavior parity is part of the proof
rectangle "01 dynamic worker\nreceive 0xCAFE\nstart dynamic timer" as dyn
rectangle "02 static worker\nreceive 0xCAFE\nstart static timer" as stat
rectangle "03 timer daemon\ndynamic callback = 1\nstatic callback = 1" as daemon
rectangle "04 verifier\nmessage parity\ncallback parity\ndistinct stacks" as verify
dyn - -> daemon
stat - -> daemon
dyn - -> verify
stat - -> verify
daemon - -> verify
@enduml
PlantUML version 1.2020.02(Sun Mar 01 11:22:07 CET 2020)
(GPL source distribution)
Java Runtime: OpenJDK Runtime Environment
JVM: OpenJDK 64-Bit Server VM
Java Version: 25.0.4-ea+4-1-Debian
Operating System: Linux
Default Encoding: UTF-8
Language: en
Country: null
--></g></svg>
Side by Side

After

Width:  |  Height:  |  Size: 6.1 KiB

web/figures/a5-flow.puml
+26
View File
@@ -0,0 +1,26 @@
@startuml
scale 540 height
skinparam backgroundColor transparent
skinparam shadowing false
skinparam defaultFontName Monospace
skinparam defaultFontSize 11
skinparam sequenceArrowColor #8095a1
title A5 FLOW — four heap checkpoints and equal behavior
participant main as M
participant "dynamic objects" as D
participant "static objects" as S
participant "scheduler / daemon" as K
participant verifier as V
M -> M : 01 H0 after static verifier
M -> D : create task + queue + timer
D --> M : 02 H1 < H0
M -> S : createStatic with named buffers
S --> M : 03 H2 = H1
M -> K : start scheduler
K -> D : 04 receive 0xCAFE; start timer
K -> S : 05 receive 0xCAFE; start timer
K -> K : 06 dynamic callback = 1
K -> K : 07 static callback = 1
K -> V : run verifier
V -> V : 08 H3 = H2; PASS + digest
@enduml
web/figures/a5-flow.svg
+38
View File
File diff suppressed because one or more lines are too long
Side by Side

After

Width:  |  Height:  |  Size: 12 KiB

web/figures/a7-runtime.puml
+18
View File
@@ -0,0 +1,18 @@
@startuml
skinparam backgroundColor transparent
skinparam shadowing false
skinparam defaultFontName Monospace
skinparam defaultFontSize 12
skinparam rectangleBorderColor #2c7794
skinparam rectangleBackgroundColor #edf6fa
title A7 RUNTIME — address provenance and heap invariants
rectangle "01 ucHeap arena\ndynamic TCB\ndynamic queue\ndynamic timer" as heap
rectangle "02 named persistent buffers\nstatic TCB + stack\nstatic queue object + storage\nstatic timer object" as bss
rectangle "03 kernel-service buffers\nIdle task\nTimer service task" as services
rectangle "04 heap relation\nH1 < H0\nH2 = H1\nH3 = H2" as relation
rectangle "05 evidence[8]\ncommit marker last\ndigest cdf44a0a" as log
heap --> relation
bss --> relation
services --> relation
relation --> log
@enduml
web/figures/a7-runtime.svg
+39
View File
@@ -0,0 +1,39 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?><svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" contentScriptType="application/ecmascript" contentStyleType="text/css" height="395px" preserveAspectRatio="none" style="width:543px;height:395px;" version="1.1" viewBox="0 0 543 395" width="543px" zoomAndPan="magnify"><defs/><g><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="317" x="116.5" y="12.8281">A7 RUNTIME — address provenance and heap invariants</text><!--MD5=[20ee4b2374ce4c140f3ed7ab4e66eea7]
entity heap--><rect fill="#EDF6FA" height="85.3765" style="stroke: #2C7794; stroke-width: 1.5;" width="116" x="6" y="24.5541"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="96" x="16" y="47.3822">01 ucHeap arena</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="73" x="16" y="63.7263">dynamic TCB</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="85" x="16" y="80.0704">dynamic queue</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="80" x="16" y="96.4145">dynamic timer</text><!--MD5=[bc98ebb1779642ad01254a57fe695731]
entity bss--><rect fill="#EDF6FA" height="85.3765" style="stroke: #2C7794; stroke-width: 1.5;" width="181" x="157.5" y="24.5541"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="158" x="167.5" y="47.3822">02 named persistent buffers</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="98" x="167.5" y="63.7263">static TCB + stack</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="161" x="167.5" y="80.0704">static queue object + storage</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="100" x="167.5" y="96.4145">static timer object</text><!--MD5=[862ebe305f068a9a150a38aa6740efca]
entity services--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="159" x="373.5" y="32.7341"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="139" x="383.5" y="55.5622">03 kernel-service buffers</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="47" x="383.5" y="71.9063">Idle task</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="102" x="383.5" y="88.2504">Timer service task</text><!--MD5=[b3e50d7f14325a04caac74353e1c3e4a]
entity relation--><rect fill="#EDF6FA" height="85.3765" style="stroke: #2C7794; stroke-width: 1.5;" width="111" x="192.5" y="169.9341"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="91" x="202.5" y="192.7622">04 heap relation</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="45" x="202.5" y="209.1063">H1 &lt; H0</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="45" x="202.5" y="225.4504">H2 = H1</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="45" x="202.5" y="241.7945">H3 = H2</text><!--MD5=[30ba7fb1050e29c0f3290b9e87c281e8]
entity log--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="129" x="183.5" y="315.3141"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="82" x="193.5" y="338.1422">05 evidence[8]</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="109" x="193.5" y="354.4863">commit marker last</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="89" x="193.5" y="370.8304">digest cdf44a0a</text><!--MD5=[02caddc9f8d8ed62a08c5abfb1f085a0]
link heap to relation--><path d="M117.72,110.1041 C140,127.4741 165.94,147.6841 188.77,165.4741 " fill="none" id="heap-&gt;relation" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="192.71,168.5341,188.0681,159.8477,188.7655,165.4614,183.1519,166.1589,192.71,168.5341" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[1b9e6995314164e9557107debb93977b]
link bss to relation--><path d="M248,110.1041 C248,126.7441 248,145.9841 248,163.2141 " fill="none" id="bss-&gt;relation" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="248,167.9541,252,158.9541,248,162.9541,244,158.9541,248,167.9541" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[7d61fe185cd425c1b673f8bc451c28cb]
link services to relation--><path d="M404.42,102.2241 C375.88,122.1841 339.54,147.6041 309.07,168.9141 " fill="none" id="services-&gt;relation" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="305.09,171.6941,314.7565,169.8076,309.1855,168.8258,310.1673,163.2548,305.09,171.6941" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[1d5a28c40c41dfb4286dc5867e2df648]
link relation to log--><path d="M248,255.6641 C248,272.4941 248,291.8141 248,308.4741 " fill="none" id="relation-&gt;log" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="248,313.4441,252,304.4441,248,308.4441,244,304.4441,248,313.4441" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[23b09fe5608adafbc0fa54b08b56f04e]
@startuml
skinparam backgroundColor transparent
skinparam shadowing false
skinparam defaultFontName Monospace
skinparam defaultFontSize 12
skinparam rectangleBorderColor #2c7794
skinparam rectangleBackgroundColor #edf6fa
title A7 RUNTIME — address provenance and heap invariants
rectangle "01 ucHeap arena\ndynamic TCB\ndynamic queue\ndynamic timer" as heap
rectangle "02 named persistent buffers\nstatic TCB + stack\nstatic queue object + storage\nstatic timer object" as bss
rectangle "03 kernel-service buffers\nIdle task\nTimer service task" as services
rectangle "04 heap relation\nH1 < H0\nH2 = H1\nH3 = H2" as relation
rectangle "05 evidence[8]\ncommit marker last\ndigest cdf44a0a" as log
heap - -> relation
bss - -> relation
services - -> relation
relation - -> log
@enduml
PlantUML version 1.2020.02(Sun Mar 01 11:22:07 CET 2020)
(GPL source distribution)
Java Runtime: OpenJDK Runtime Environment
JVM: OpenJDK 64-Bit Server VM
Java Version: 25.0.4-ea+4-1-Debian
Operating System: Linux
Default Encoding: UTF-8
Language: en
Country: null
--></g></svg>
Side by Side

After

Width:  |  Height:  |  Size: 6.7 KiB