feat: publish FreeRTOS C FC10 card
This commit is contained in:
Binary file not shown.
|
After Width: | Height: | Size: 23 KiB |
@@ -0,0 +1,20 @@
|
||||
@startuml
|
||||
skinparam backgroundColor transparent
|
||||
skinparam shadowing false
|
||||
skinparam defaultFontName Monospace
|
||||
skinparam defaultFontSize 12
|
||||
skinparam rectangleBorderColor #2c7794
|
||||
skinparam rectangleBackgroundColor #edf6fa
|
||||
title A2 STRUCTURE — notification slot belongs to target TCB
|
||||
rectangle "01 Sender p3\nTaskHandle_t receiver" as sender
|
||||
rectangle "02 Receiver TCB\nnotification[0]\nvalue + pending state" as receiver
|
||||
rectangle "03 COUNT mode\nthree increments\nulTaskNotifyTake" as count
|
||||
rectangle "04 OVERWRITE mode\n0x11 → 0x22\nxTaskNotifyWait" as overwrite
|
||||
rectangle "05 BITS mode\n0x04 OR 0x20 = 0x24" as bits
|
||||
rectangle "06 no queue object\nno EventGroup object\none target only" as absent
|
||||
sender --> receiver : direct binding
|
||||
receiver --> count
|
||||
receiver --> overwrite
|
||||
receiver --> bits
|
||||
receiver ..> absent
|
||||
@enduml
|
||||
@@ -0,0 +1,43 @@
|
||||
<?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="365px" preserveAspectRatio="none" style="width:652px;height:365px;" version="1.1" viewBox="0 0 652 365" width="652px" zoomAndPan="magnify"><defs/><g><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="313" x="173" y="12.8281">A2 STRUCTURE — notification slot belongs to target TCB</text><!--MD5=[b84dfc3c68caa5bb5eca96917ddde04e]
|
||||
entity sender--><rect fill="#EDF6FA" height="52.6882" style="stroke: #2C7794; stroke-width: 1.5;" width="144" x="240" y="24.5941"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="74" x="250" y="47.4222">01 Sender p3</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="124" x="250" y="63.7663">TaskHandle_t receiver</text><!--MD5=[5396727a6920f555e89155bb37322e73]
|
||||
entity receiver--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="139" x="242.5" y="155.2841"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="91" x="252.5" y="178.1122">02 Receiver TCB</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="77" x="252.5" y="194.4563">notification[0]</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="119" x="252.5" y="210.8004">value + pending state</text><!--MD5=[a6c46d55ef9c7049dd227ea88955dfe5]
|
||||
entity count--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="116" x="6" y="285.3141"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="94" x="16" y="308.1422">03 COUNT mode</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="96" x="16" y="324.4863">three increments</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="96" x="16" y="340.8304">ulTaskNotifyTake</text><!--MD5=[ce9509fd5e871a6a83b28f49ecacc291]
|
||||
entity overwrite--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="138" x="157" y="285.3141"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="118" x="167" y="308.1422">04 OVERWRITE mode</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="70" x="167" y="324.4863">0x11 → 0x22</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="90" x="167" y="340.8304">xTaskNotifyWait</text><!--MD5=[dbf1c5340e3c6dc08db3ffddcb8b49cb]
|
||||
entity bits--><rect fill="#EDF6FA" height="52.6882" style="stroke: #2C7794; stroke-width: 1.5;" width="136" x="330" y="293.4841"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="78" x="340" y="316.3122">05 BITS mode</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="116" x="340" y="332.6563">0x04 OR 0x20 = 0x24</text><!--MD5=[e6866c9fa1d9b487354cb76589f44590]
|
||||
entity absent--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="140" x="501" y="285.3141"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="106" x="511" y="308.1422">06 no queue object</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="120" x="511" y="324.4863">no EventGroup object</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="84" x="511" y="340.8304">one target only</text><!--MD5=[8e9d1a540edca769c23c091c682d9a7a]
|
||||
link sender to receiver--><path d="M312,77.6741 C312,97.6341 312,125.6641 312,148.5741 " fill="none" id="sender->receiver" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="312,153.3741,316,144.3741,312,148.3741,308,144.3741,312,153.3741" style="stroke: #A80036; stroke-width: 1.0;"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="76" x="313" y="121.1122">direct binding</text><!--MD5=[dbdb0cc6f73e70c89a117f8b5d5c3472]
|
||||
link receiver to count--><path d="M246.19,224.7741 C209.69,243.6141 164.48,266.9541 128.23,285.6641 " fill="none" id="receiver->count" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="123.84,287.9341,133.6729,287.3737,128.2861,285.6467,130.0131,280.2599,123.84,287.9341" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[bdde82900f0d2fcfa2bd2764e99964d9]
|
||||
link receiver to overwrite--><path d="M289.18,224.7741 C277.82,241.6841 264.02,262.2241 252.22,279.7941 " fill="none" id="receiver->overwrite" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="249.47,283.8841,257.8113,278.6475,252.26,279.7349,251.1726,274.1835,249.47,283.8841" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[bbe09b516f396593785a1b5b082d3f1c]
|
||||
link receiver to bits--><path d="M334.82,224.7741 C348.01,244.4041 364.48,268.9241 377.29,288.0041 " fill="none" id="receiver->bits" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="379.96,291.9741,378.2728,282.2708,377.1766,287.8205,371.627,286.7242,379.96,291.9741" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[913cacc1ea3cf574ad7e42ca9161fb6f]
|
||||
link receiver to absent--><path d="M380.73,224.7741 C416.43,242.4241 460.11,264.0141 496.61,282.0541 " fill="none" id="receiver->absent" style="stroke: #A80036; stroke-width: 1.0; stroke-dasharray: 7.0,7.0;"/><polygon fill="#A80036" points="501.04,284.2441,494.7403,276.6736,496.5565,282.0309,491.1991,283.8472,501.04,284.2441" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[66fdc3bd0d492b4ef1961d02cd2282a3]
|
||||
@startuml
|
||||
skinparam backgroundColor transparent
|
||||
skinparam shadowing false
|
||||
skinparam defaultFontName Monospace
|
||||
skinparam defaultFontSize 12
|
||||
skinparam rectangleBorderColor #2c7794
|
||||
skinparam rectangleBackgroundColor #edf6fa
|
||||
title A2 STRUCTURE — notification slot belongs to target TCB
|
||||
rectangle "01 Sender p3\nTaskHandle_t receiver" as sender
|
||||
rectangle "02 Receiver TCB\nnotification[0]\nvalue + pending state" as receiver
|
||||
rectangle "03 COUNT mode\nthree increments\nulTaskNotifyTake" as count
|
||||
rectangle "04 OVERWRITE mode\n0x11 → 0x22\nxTaskNotifyWait" as overwrite
|
||||
rectangle "05 BITS mode\n0x04 OR 0x20 = 0x24" as bits
|
||||
rectangle "06 no queue object\nno EventGroup object\none target only" as absent
|
||||
sender - -> receiver : direct binding
|
||||
receiver - -> count
|
||||
receiver - -> overwrite
|
||||
receiver - -> bits
|
||||
receiver ..> absent
|
||||
@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>
|
||||
|
After Width: | Height: | Size: 7.2 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 15 KiB |
@@ -0,0 +1,18 @@
|
||||
@startuml
|
||||
skinparam backgroundColor transparent
|
||||
skinparam shadowing false
|
||||
skinparam defaultFontName Monospace
|
||||
skinparam defaultFontSize 12
|
||||
skinparam rectangleBorderColor #2c7794
|
||||
skinparam rectangleBackgroundColor #edf6fa
|
||||
title A3 DISPATCH — handle selects exactly one notification slot
|
||||
rectangle "01 sender code" as sender
|
||||
rectangle "02 receiver_handle" as handle
|
||||
rectangle "03 xTaskGenericNotify\nindex 0\naction" as api
|
||||
rectangle "04 target TCB\nulNotifiedValue[0]\nucNotifyState[0]" as tcb
|
||||
rectangle "05 receiver Ready\nonly if waiting" as ready
|
||||
sender --> handle
|
||||
handle --> api
|
||||
api --> tcb
|
||||
tcb --> ready
|
||||
@enduml
|
||||
@@ -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="538px" preserveAspectRatio="none" style="width:343px;height:538px;" version="1.1" viewBox="0 0 343 538" width="343px" zoomAndPan="magnify"><defs/><g><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="329" x="2" y="12.8281">A3 DISPATCH — handle selects exactly one notification slot</text><!--MD5=[b84dfc3c68caa5bb5eca96917ddde04e]
|
||||
entity sender--><rect fill="#EDF6FA" height="36.3441" style="stroke: #2C7794; stroke-width: 1.5;" width="106" x="107.5" y="23.9041"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="86" x="117.5" y="46.7322">01 sender code</text><!--MD5=[4a4e163a39735e62fba287d6513b540f]
|
||||
entity handle--><rect fill="#EDF6FA" height="36.3441" style="stroke: #2C7794; stroke-width: 1.5;" width="126" x="97.5" y="120.2441"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="106" x="107.5" y="143.0722">02 receiver_handle</text><!--MD5=[e2307af040e3f87d22824e7603ca28ec]
|
||||
entity api--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="146" x="87.5" y="216.5941"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="126" x="97.5" y="239.4222">03 xTaskGenericNotify</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="40" x="97.5" y="255.7663">index 0</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="34" x="97.5" y="272.1104">action</text><!--MD5=[0bb6f33dfd49e802fce6b5273bbb9861]
|
||||
entity tcb--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="120" x="100.5" y="345.6241"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="77" x="110.5" y="368.4522">04 target TCB</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="100" x="110.5" y="384.7963">ulNotifiedValue[0]</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="90" x="110.5" y="401.1404">ucNotifyState[0]</text><!--MD5=[55a3d76f9f066a914db2e6a0219879c4]
|
||||
entity ready--><rect fill="#EDF6FA" height="52.6882" style="stroke: #2C7794; stroke-width: 1.5;" width="120" x="100.5" y="474.6541"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="100" x="110.5" y="497.4822">05 receiver Ready</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="76" x="110.5" y="513.8263">only if waiting</text><!--MD5=[05c26f944d0154c81d61b2d29bfe9b94]
|
||||
link sender to handle--><path d="M160.5,60.3841 C160.5,75.3141 160.5,97.0341 160.5,113.6041 " fill="none" id="sender->handle" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="160.5,118.3941,164.5,109.3941,160.5,113.3941,156.5,109.3941,160.5,118.3941" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[f548c039a31678651f5704e87a20a29c]
|
||||
link handle to api--><path d="M160.5,156.7141 C160.5,171.0241 160.5,191.9141 160.5,210.3141 " fill="none" id="handle->api" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="160.5,214.9341,164.5,205.9341,160.5,209.9341,156.5,205.9341,160.5,214.9341" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[21608e01fc85af78623daa24c4ba84aa]
|
||||
link api to tcb--><path d="M160.5,285.8141 C160.5,302.1841 160.5,321.9641 160.5,339.0941 " fill="none" id="api->tcb" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="160.5,343.7641,164.5,334.7641,160.5,338.7641,156.5,334.7641,160.5,343.7641" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[a3b483e3e56f4509be0568c8901afffe]
|
||||
link tcb to ready--><path d="M160.5,414.8841 C160.5,431.6041 160.5,451.6841 160.5,468.1441 " fill="none" id="tcb->ready" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="160.5,472.9741,164.5,463.9741,160.5,467.9741,156.5,463.9741,160.5,472.9741" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[500876efc367c503fbb666963fffec2c]
|
||||
@startuml
|
||||
skinparam backgroundColor transparent
|
||||
skinparam shadowing false
|
||||
skinparam defaultFontName Monospace
|
||||
skinparam defaultFontSize 12
|
||||
skinparam rectangleBorderColor #2c7794
|
||||
skinparam rectangleBackgroundColor #edf6fa
|
||||
title A3 DISPATCH — handle selects exactly one notification slot
|
||||
rectangle "01 sender code" as sender
|
||||
rectangle "02 receiver_handle" as handle
|
||||
rectangle "03 xTaskGenericNotify\nindex 0\naction" as api
|
||||
rectangle "04 target TCB\nulNotifiedValue[0]\nucNotifyState[0]" as tcb
|
||||
rectangle "05 receiver Ready\nonly if waiting" as ready
|
||||
sender - -> handle
|
||||
handle - -> api
|
||||
api - -> tcb
|
||||
tcb - -> ready
|
||||
@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>
|
||||
|
After Width: | Height: | Size: 5.3 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 34 KiB |
@@ -0,0 +1,29 @@
|
||||
@startuml
|
||||
scale 520 height
|
||||
skinparam backgroundColor transparent
|
||||
skinparam shadowing false
|
||||
skinparam defaultFontName Monospace
|
||||
skinparam defaultFontSize 11
|
||||
skinparam sequenceArrowColor #8095a1
|
||||
title A5 FLOW — three notification protocols on one target slot
|
||||
participant "Sender p3" as S
|
||||
participant "Receiver p2" as R
|
||||
participant "TCB notify[0]" as N
|
||||
participant "Verifier p0" as V
|
||||
S -> S : 02 arm; wait for phase 1 + Blocked
|
||||
R -> N : 03 ulTaskNotifyTake(clear); Blocked
|
||||
S -> N : give + give + give
|
||||
S -> S : 04 receiver was Blocked; value=3
|
||||
N --> R : 05 return 3; clear value
|
||||
R -> N : 06 probe zero; wait overwrite
|
||||
S -> N : overwrite 0x11; overwrite 0x22
|
||||
S -> S : 07 receiver was Blocked
|
||||
N --> R : 08 return 0x22; clear value
|
||||
R -> N : 09 probe zero; wait bits
|
||||
S -> N : setBits 0x04; setBits 0x20
|
||||
S -> S : 10 receiver was Blocked
|
||||
N --> R : 11 return 0x24; clear value
|
||||
R -> V : completed
|
||||
S -> V : completed
|
||||
V -> V : 12 PASS + digest
|
||||
@enduml
|
||||
File diff suppressed because one or more lines are too long
|
After Width: | Height: | Size: 13 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 14 KiB |
@@ -0,0 +1,23 @@
|
||||
@startuml
|
||||
scale 700 height
|
||||
skinparam backgroundColor transparent
|
||||
skinparam shadowing false
|
||||
skinparam defaultFontName Monospace
|
||||
skinparam defaultFontSize 12
|
||||
skinparam stateBorderColor #2c7794
|
||||
skinparam stateBackgroundColor #edf6fa
|
||||
title A6 STATE — value and pending are separate state
|
||||
[*] --> ClearCount : 01 value=0 / not pending
|
||||
ClearCount --> WaitingCount : 03 wait
|
||||
WaitingCount --> Count3 : 04 three gives
|
||||
Count3 --> ClearOverwrite : 05 take(pdTRUE) returns 3
|
||||
ClearOverwrite --> WaitingOverwrite : 06 wait
|
||||
WaitingOverwrite --> Value11 : overwrite 0x11
|
||||
Value11 --> Value22 : overwrite 0x22
|
||||
Value22 --> ClearBits : 08 wait returns 0x22
|
||||
ClearBits --> WaitingBits : 09 wait
|
||||
WaitingBits --> Bits04 : set 0x04
|
||||
Bits04 --> Bits24 : OR 0x20
|
||||
Bits24 --> ClearDone : 11 wait returns 0x24
|
||||
ClearDone --> [*] : 12 PASS
|
||||
@enduml
|
||||
File diff suppressed because one or more lines are too long
|
After Width: | Height: | Size: 15 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 24 KiB |
@@ -0,0 +1,21 @@
|
||||
@startuml
|
||||
skinparam backgroundColor transparent
|
||||
skinparam shadowing false
|
||||
skinparam defaultFontName Monospace
|
||||
skinparam defaultFontSize 12
|
||||
skinparam rectangleBorderColor #2c7794
|
||||
skinparam rectangleBackgroundColor #edf6fa
|
||||
title A7 RUNTIME — public proof and TCB debugger evidence
|
||||
rectangle "01 g_fc10\nreceiver handle\nphase + results" as exp
|
||||
rectangle "02 sender stack\np3 during posts" as sender
|
||||
rectangle "03 receiver stack\neBlocked before each phase" as receiver
|
||||
rectangle "04 notification slot 0\nvalue 0→3→0→0x22→0→0x24→0\n(debugger evidence)" as slot
|
||||
rectangle "05 no intermediary object\nsmaller topology than queue/semaphore" as absent
|
||||
rectangle "06 events[12]\ncommit marker last\ndigest c60747cb" as log
|
||||
exp --> sender
|
||||
exp --> receiver
|
||||
receiver ..> slot
|
||||
exp ..> absent
|
||||
sender --> log
|
||||
receiver --> log
|
||||
@enduml
|
||||
@@ -0,0 +1,45 @@
|
||||
<?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="346px" preserveAspectRatio="none" style="width:631px;height:346px;" version="1.1" viewBox="0 0 631 346" width="631px" zoomAndPan="magnify"><defs/><g><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="316" x="161" y="12.8281">A7 RUNTIME — public proof and TCB debugger evidence</text><!--MD5=[761712401e76352e16e0203320c8b9d5]
|
||||
entity exp--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="107" x="195" y="24.5941"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="53" x="205" y="47.4222">01 g_fc10</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="87" x="205" y="63.7663">receiver handle</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="85" x="205" y="80.1104">phase + results</text><!--MD5=[b84dfc3c68caa5bb5eca96917ddde04e]
|
||||
entity sender--><rect fill="#EDF6FA" height="52.6882" style="stroke: #2C7794; stroke-width: 1.5;" width="108" x="16.5" y="153.6241"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="88" x="26.5" y="176.4522">02 sender stack</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="86" x="26.5" y="192.7963">p3 during posts</text><!--MD5=[5396727a6920f555e89155bb37322e73]
|
||||
entity receiver--><rect fill="#EDF6FA" height="52.6882" style="stroke: #2C7794; stroke-width: 1.5;" width="178" x="159.5" y="153.6241"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="95" x="169.5" y="176.4522">03 receiver stack</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="158" x="169.5" y="192.7963">eBlocked before each phase</text><!--MD5=[43dd893c4b9fb4e2e35d3b50f2a106fd]
|
||||
entity slot--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="202" x="170.5" y="266.3141"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="112" x="180.5" y="289.1422">04 notification slot 0</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="182" x="180.5" y="305.4863">value 0→3→0→0x22→0→0x24→0</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="115" x="180.5" y="321.8304">(debugger evidence)</text><!--MD5=[e6866c9fa1d9b487354cb76589f44590]
|
||||
entity absent--><rect fill="#EDF6FA" height="52.6882" style="stroke: #2C7794; stroke-width: 1.5;" width="247" x="373" y="153.6241"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="143" x="383" y="176.4522">05 no intermediary object</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="227" x="383" y="192.7963">smaller topology than queue/semaphore</text><!--MD5=[30ba7fb1050e29c0f3290b9e87c281e8]
|
||||
entity log--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="129" x="6" y="266.3141"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="76" x="16" y="289.1422">06 events[12]</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="109" x="16" y="305.4863">commit marker last</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="91" x="16" y="321.8304">digest c60747cb</text><!--MD5=[8192d8ff185c7ccf4d18c9500b30058a]
|
||||
link exp to sender--><path d="M197.97,93.8541 C171.58,111.4741 139.61,132.8241 114.28,149.7341 " fill="none" id="exp->sender" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="110.24,152.4341,119.9473,150.77,114.4003,149.6606,115.5097,144.1136,110.24,152.4341" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[0e8eba5a1d4fe2aa425220f12f10d925]
|
||||
link exp to receiver--><path d="M248.5,93.8541 C248.5,110.5741 248.5,130.6541 248.5,147.1141 " fill="none" id="exp->receiver" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="248.5,151.9441,252.5,142.9441,248.5,146.9441,244.5,142.9441,248.5,151.9441" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[f617065c14176a4279cfca53fbdf0025]
|
||||
link receiver to slot--><path d="M253.49,206.7541 C256.48,222.2041 260.34,242.1741 263.72,259.6441 " fill="none" id="receiver->slot" style="stroke: #A80036; stroke-width: 1.0; stroke-dasharray: 7.0,7.0;"/><polygon fill="#A80036" points="264.66,264.4741,266.8925,254.8816,263.7179,259.5637,259.0358,256.389,264.66,264.4741" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[8bbd53190c2d42e09e3094ea620607fc]
|
||||
link exp to absent--><path d="M302.31,85.8941 C342.04,104.9441 396.1,130.8541 437.1,150.4941 " fill="none" id="exp->absent" style="stroke: #A80036; stroke-width: 1.0; stroke-dasharray: 7.0,7.0;"/><polygon fill="#A80036" points="441.43,152.5741,435.0534,145.0682,436.9242,150.4068,431.5856,152.2775,441.43,152.5741" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[06d1517c0e62c3411479bff3ba90e42f]
|
||||
link sender to log--><path d="M70.5,206.7541 C70.5,222.2041 70.5,242.1741 70.5,259.6441 " fill="none" id="sender->log" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="70.5,264.4441,74.5,255.4441,70.5,259.4441,66.5,255.4441,70.5,264.4441" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[2ceaba7302568f3c50768477380e08af]
|
||||
link receiver to log--><path d="M209.88,206.7541 C185.53,223.0141 153.68,244.2841 126.58,262.3841 " fill="none" id="receiver->log" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="122.48,265.1141,132.1873,263.45,126.6403,262.3406,127.7497,256.7936,122.48,265.1141" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[24d6ab3206fcf8ec9d4761d0cefdb88f]
|
||||
@startuml
|
||||
skinparam backgroundColor transparent
|
||||
skinparam shadowing false
|
||||
skinparam defaultFontName Monospace
|
||||
skinparam defaultFontSize 12
|
||||
skinparam rectangleBorderColor #2c7794
|
||||
skinparam rectangleBackgroundColor #edf6fa
|
||||
title A7 RUNTIME — public proof and TCB debugger evidence
|
||||
rectangle "01 g_fc10\nreceiver handle\nphase + results" as exp
|
||||
rectangle "02 sender stack\np3 during posts" as sender
|
||||
rectangle "03 receiver stack\neBlocked before each phase" as receiver
|
||||
rectangle "04 notification slot 0\nvalue 0→3→0→0x22→0→0x24→0\n(debugger evidence)" as slot
|
||||
rectangle "05 no intermediary object\nsmaller topology than queue/semaphore" as absent
|
||||
rectangle "06 events[12]\ncommit marker last\ndigest c60747cb" as log
|
||||
exp - -> sender
|
||||
exp - -> receiver
|
||||
receiver ..> slot
|
||||
exp ..> absent
|
||||
sender - -> log
|
||||
receiver - -> 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>
|
||||
|
After Width: | Height: | Size: 7.3 KiB |
Binary file not shown.
|
After Width: | Height: | Size: 16 KiB |
@@ -0,0 +1,16 @@
|
||||
@startuml
|
||||
skinparam backgroundColor transparent
|
||||
skinparam shadowing false
|
||||
skinparam defaultFontName Monospace
|
||||
skinparam defaultFontSize 12
|
||||
skinparam rectangleBorderColor #2c7794
|
||||
skinparam rectangleBackgroundColor #edf6fa
|
||||
title A8 PATTERNS — choose notification action by information contract
|
||||
rectangle "01 GIVE / TAKE\ncount occurrences\npdTRUE clears all\npdFALSE decrements one" as count
|
||||
rectangle "02 OVERWRITE\nlatest state wins\nintermediate state may be lost" as overwrite
|
||||
rectangle "03 SET BITS\ncombine independent flags\nOR semantics" as bits
|
||||
rectangle "04 limitations\none target per handle\nnot broadcast\nnot a general queue" as limits
|
||||
count -[hidden]right- overwrite
|
||||
overwrite -[hidden]right- bits
|
||||
bits --> limits
|
||||
@enduml
|
||||
@@ -0,0 +1,35 @@
|
||||
<?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="266px" preserveAspectRatio="none" style="width:610px;height:266px;" version="1.1" viewBox="0 0 610 266" width="610px" zoomAndPan="magnify"><defs/><g><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="370" x="124" y="12.8281">A8 PATTERNS — choose notification action by information contract</text><!--MD5=[a6c46d55ef9c7049dd227ea88955dfe5]
|
||||
entity count--><rect fill="#EDF6FA" height="85.3765" style="stroke: #2C7794; stroke-width: 1.5;" width="162" x="6" y="24.5941"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="83" x="16" y="47.4222">01 GIVE / TAKE</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="103" x="16" y="63.7663">count occurrences</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="97" x="16" y="80.1104">pdTRUE clears all</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="142" x="16" y="96.4545">pdFALSE decrements one</text><!--MD5=[ce9509fd5e871a6a83b28f49ecacc291]
|
||||
entity overwrite--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="190" x="203" y="32.7641"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="83" x="213" y="55.5922">02 OVERWRITE</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="90" x="213" y="71.9363">latest state wins</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="170" x="213" y="88.2804">intermediate state may be lost</text><!--MD5=[dbf1c5340e3c6dc08db3ffddcb8b49cb]
|
||||
entity bits--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="171" x="428.5" y="32.7641"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="67" x="438.5" y="55.5922">03 SET BITS</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="151" x="438.5" y="71.9363">combine independent flags</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="76" x="438.5" y="88.2804">OR semantics</text><!--MD5=[5d1e2e604515e778cc92ad38d01c5107]
|
||||
entity limits--><rect fill="#EDF6FA" height="85.3765" style="stroke: #2C7794; stroke-width: 1.5;" width="141" x="443.5" y="169.9641"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="75" x="453.5" y="192.7922">04 limitations</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="121" x="453.5" y="209.1363">one target per handle</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="77" x="453.5" y="225.4804">not broadcast</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="112" x="453.5" y="241.8245">not a general queue</text><!--MD5=[8a8e32e48dd9a6558a97ec9f8b34730d]
|
||||
link count to overwrite--><!--MD5=[97200929cb575c759242ec792e7421f8]
|
||||
link overwrite to bits--><!--MD5=[407848b4f0f1fa209f6d0eaf3831b5ba]
|
||||
link bits to limits--><path d="M514,102.2541 C514,120.4941 514,143.2741 514,163.3141 " fill="none" id="bits->limits" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="514,168.2041,518,159.2041,514,163.2041,510,159.2041,514,168.2041" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[8793ce5dc13c7b7e1911bbeaf7c404d4]
|
||||
@startuml
|
||||
skinparam backgroundColor transparent
|
||||
skinparam shadowing false
|
||||
skinparam defaultFontName Monospace
|
||||
skinparam defaultFontSize 12
|
||||
skinparam rectangleBorderColor #2c7794
|
||||
skinparam rectangleBackgroundColor #edf6fa
|
||||
title A8 PATTERNS — choose notification action by information contract
|
||||
rectangle "01 GIVE / TAKE\ncount occurrences\npdTRUE clears all\npdFALSE decrements one" as count
|
||||
rectangle "02 OVERWRITE\nlatest state wins\nintermediate state may be lost" as overwrite
|
||||
rectangle "03 SET BITS\ncombine independent flags\nOR semantics" as bits
|
||||
rectangle "04 limitations\none target per handle\nnot broadcast\nnot a general queue" as limits
|
||||
count -[hidden]right- overwrite
|
||||
overwrite -[hidden]right- bits
|
||||
bits - -> limits
|
||||
@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>
|
||||
|
After Width: | Height: | Size: 4.9 KiB |
Reference in New Issue
Block a user