134 lines
15 KiB
XML
134 lines
15 KiB
XML
<?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="324.9253px" preserveAspectRatio="none" style="width:896px;height:324px;" version="1.1" viewBox="0 0 896 324" width="896.2343px" zoomAndPan="magnify"><defs/><g><!--MD5=[24a425f7d3746dcb4595e0db6477f052]
|
|
class Peers--><rect fill="#F5F8FA" height="126.4532" id="Peers" style="stroke: #607985; stroke-width: 0.8069336521219366;" width="172.1458" x="192.5882" y="74.5069"/><text fill="#526B77" font-family="DejaVu Sans Mono" font-size="5.9175" font-style="italic" lengthAdjust="spacingAndGlyphs" textLength="37.6569" x="259.8326" y="85.9172">«C struct»</text><text fill="#1F3039" font-family="DejaVu Sans Mono" font-size="8.0693" lengthAdjust="spacingAndGlyphs" textLength="91.9904" x="232.6659" y="101.2584">01 PeerContext [2]</text><line style="stroke: #607985; stroke-width: 0.8069336521219366;" x1="193.1261" x2="364.1961" y1="109.0789" y2="109.0789"/><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="55.9474" x="199.0436" y="120.95">id : uint32_t</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="159.2349" x="199.0436" y="135.5462">configured_priority : UBaseType_t = 2</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="90.3766" x="199.0436" y="150.1425">handle : TaskHandle_t</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="90.3766" x="199.0436" y="164.7387">iterations · checksum</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="94.6802" x="199.0436" y="179.335">first_tick · last_tick</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="94.6802" x="199.0436" y="193.9312">entry_sp · stack range</text><!--MD5=[07843a28108f8f9fb73050ea95a4c52b]
|
|
class Probe--><rect fill="#F5F8FA" height="111.857" id="Probe" style="stroke: #607985; stroke-width: 0.8069336521219366;" width="124.8057" x="562.9707" y="207.6886"/><text fill="#526B77" font-family="DejaVu Sans Mono" font-size="5.9175" font-style="italic" lengthAdjust="spacingAndGlyphs" textLength="37.6569" x="606.5451" y="219.0989">«C struct»</text><text fill="#1F3039" font-family="DejaVu Sans Mono" font-size="8.0693" lengthAdjust="spacingAndGlyphs" textLength="96.832" x="576.9576" y="234.4401">02 HighProbeContext</text><line style="stroke: #607985; stroke-width: 0.8069336521219366;" x1="563.5087" x2="687.2385" y1="242.2606" y2="242.2606"/><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="86.0729" x="569.4262" y="254.1317">initial_priority = 0</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="81.7693" x="569.4262" y="268.7279">target_priority = 3</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="90.3766" x="569.4262" y="283.3242">handle : TaskHandle_t</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="34.4292" x="569.4262" y="297.9204">run_tick</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="111.8948" x="569.4262" y="312.5167">ran_before_caller_returned</text><!--MD5=[ec6b96eb83f6cad8feb931a71676c16d]
|
|
class Verify--><rect fill="#F5F8FA" height="82.6645" id="Verify" style="stroke: #607985; stroke-width: 0.8069336521219366;" width="111.8948" x="3.2277" y="196.9994"/><text fill="#526B77" font-family="DejaVu Sans Mono" font-size="5.9175" font-style="italic" lengthAdjust="spacingAndGlyphs" textLength="37.6569" x="40.3467" y="208.4097">«C struct»</text><text fill="#1F3039" font-family="DejaVu Sans Mono" font-size="8.0693" lengthAdjust="spacingAndGlyphs" textLength="91.9904" x="13.1799" y="223.7509">03 VerifierContext</text><line style="stroke: #607985; stroke-width: 0.8069336521219366;" x1="3.7657" x2="114.5846" y1="231.5715" y2="231.5715"/><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="98.9839" x="9.6832" y="243.4425">configured_priority = 1</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="90.3766" x="9.6832" y="258.0387">handle : TaskHandle_t</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="17.2146" x="9.6832" y="272.635">pass</text><!--MD5=[052633df24897554133d204f5acba5bb]
|
|
class SwitchTrace--><rect fill="#F5F8FA" height="97.2607" id="SwitchTrace" style="stroke: #607985; stroke-width: 0.8069336521219366;" width="102.2116" x="574.2678" y="44.9946"/><text fill="#526B77" font-family="DejaVu Sans Mono" font-size="5.9175" font-style="italic" lengthAdjust="spacingAndGlyphs" textLength="60.251" x="595.2481" y="56.4049">«bounded record»</text><text fill="#1F3039" font-family="DejaVu Sans Mono" font-size="8.0693" lengthAdjust="spacingAndGlyphs" textLength="77.4656" x="586.6408" y="71.7461">04 switch trace</text><line style="stroke: #607985; stroke-width: 0.8069336521219366;" x1="574.8057" x2="675.9414" y1="79.5667" y2="79.5667"/><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="34.4292" x="580.7233" y="91.4377">task[16]</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="34.4292" x="580.7233" y="106.034">tick[16]</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="64.5547" x="580.7233" y="120.6302">count · changes</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="77.4656" x="580.7233" y="135.2265">captured A · B · A</text><!--MD5=[903c07076df7fb06c97b1a15577bcab5]
|
|
class OrderTrace--><rect fill="#F5F8FA" height="82.6645" id="OrderTrace" style="stroke: #607985; stroke-width: 0.8069336521219366;" width="116.1984" x="774.1184" y="93.7119"/><text fill="#526B77" font-family="DejaVu Sans Mono" font-size="5.9175" font-style="italic" lengthAdjust="spacingAndGlyphs" textLength="60.251" x="802.0921" y="105.1222">«bounded record»</text><text fill="#1F3039" font-family="DejaVu Sans Mono" font-size="8.0693" lengthAdjust="spacingAndGlyphs" textLength="106.5152" x="778.96" y="120.4634">05 preemption markers</text><line style="stroke: #607985; stroke-width: 0.8069336521219366;" x1="774.6563" x2="889.7788" y1="128.284" y2="128.284"/><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="68.8583" x="780.5738" y="140.155">1 = before_raise</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="60.251" x="780.5738" y="154.7512">2 = high_probe</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="6.9934" lengthAdjust="spacingAndGlyphs" textLength="64.5547" x="780.5738" y="169.3475">3 = after_raise</text><path d="M541.1835,161.4244 L541.1835,188.2886 A0,0 0 0 0 541.1835,188.2886 L709.5637,188.2886 A0,0 0 0 0 709.5637,188.2886 L709.5637,166.8039 L704.1841,161.4244 L627.5254,161.4244 L625.3736,142.4668 L623.2218,161.4244 L541.1835,161.4244 A0,0 0 0 0 541.1835,161.4244 " fill="#F7F5ED" style="stroke: #8A887C; stroke-width: 0.5379557680812911;"/><path d="M704.1841,161.4244 L704.1841,166.8039 L709.5637,166.8039 L704.1841,161.4244 " fill="#F7F5ED" style="stroke: #8A887C; stroke-width: 0.5379557680812911;"/><text fill="#3E4B50" font-family="DejaVu Sans Mono" font-size="6.4555" lengthAdjust="spacingAndGlyphs" textLength="124.2678" x="547.639" y="173.334">A→B→A is a committed subsequence.</text><text fill="#3E4B50" font-family="DejaVu Sans Mono" font-size="6.4555" lengthAdjust="spacingAndGlyphs" textLength="150.6276" x="547.639" y="180.8486">Repeated loop iterations are not logged.</text><!--MD5=[96579476f064ff1ffa3f552d3ff15ad8]
|
|
link Peers to SwitchTrace--><path d="M364.8577,126.8016 C429.2833,118.5816 515.5983,107.5643 570.728,100.5278 " fill="none" id="Peers->SwitchTrace" style="stroke: #607985; stroke-width: 0.6993424985056784;"/><polygon fill="#607985" points="573.3425,100.1943,568.2687,98.6686,570.6741,100.5326,568.81,102.938,573.3425,100.1943" style="stroke: #607985; stroke-width: 0.6993424985056784;"/><text fill="#425B67" font-family="DejaVu Sans Mono" font-size="7.5314" lengthAdjust="spacingAndGlyphs" textLength="146.324" x="379.7968" y="101.2783">one entry per observed task change</text><!--MD5=[e0cf694b28b62e4fb8bc23e78e5c0c4e]
|
|
link Peers to Probe--><path d="M364.8577,168.9342 C425.0873,190.8667 504.4411,219.7711 559.5655,239.8476 " fill="none" id="Peers->Probe" style="stroke: #607985; stroke-width: 0.6993424985056784;"/><polygon fill="#607985" points="562.0669,240.7567,558.2558,237.0762,559.54,239.835,556.7811,241.1193,562.0669,240.7567" style="stroke: #607985; stroke-width: 0.6993424985056784;"/><text fill="#425B67" font-family="DejaVu Sans Mono" font-size="7.5314" lengthAdjust="spacingAndGlyphs" textLength="116.1984" x="394.8595" y="169.5503">vTaskPrioritySet(handle, 3)</text><!--MD5=[5dc87c6eff7493b6adeed17dd71f1a79]
|
|
link Probe to OrderTrace--><path d="M687.9271,224.8655 C714.303,208.3879 744.9558,189.2367 771.165,172.8613 " fill="none" id="Probe->OrderTrace" style="stroke: #607985; stroke-width: 0.6993424985056784;"/><polygon fill="#607985" points="773.3168,171.5111,768.0707,172.2524,771.0359,172.9366,770.3516,175.9018,773.3168,171.5111" style="stroke: #607985; stroke-width: 0.6993424985056784;"/><text fill="#425B67" font-family="DejaVu Sans Mono" font-size="7.5314" lengthAdjust="spacingAndGlyphs" textLength="34.4292" x="724.6264" y="174.9191">marker 2</text><!--MD5=[16ba7551656b4926f6566f6281eca0fa]
|
|
link Peers to OrderTrace--><path d="M364.89,88.8273 C452.8942,45.1829 593.0801,-5.9283 709.5637,35.5266 C741.1363,46.7591 770.4603,70.0418 792.4573,91.2642 " fill="none" id="Peers->OrderTrace" style="stroke: #607985; stroke-width: 0.6993424985056784;"/><polygon fill="#607985" points="794.2487,93.0072,792.2868,88.0855,792.3237,91.1285,789.2808,91.1654,794.2487,93.0072" style="stroke: #607985; stroke-width: 0.6993424985056784;"/><text fill="#425B67" font-family="DejaVu Sans Mono" font-size="7.5314" lengthAdjust="spacingAndGlyphs" textLength="64.5547" x="593.0962" y="14.8288">markers 1 and 3</text><!--MD5=[5305fbff9ac0c80de73336ac373d19f8]
|
|
link Verify to Peers--><path d="M115.2516,212.7507 C137.7812,202.379 164.3616,190.1351 189.4465,178.5798 " fill="none" id="Verify->Peers" style="stroke: #607985; stroke-width: 0.6993424985056784;"/><polygon fill="#607985" points="191.7597,177.5146,186.462,177.593,189.3182,178.6433,188.2679,181.4994,191.7597,177.5146" style="stroke: #607985; stroke-width: 0.6993424985056784;"/><text fill="#425B67" font-family="DejaVu Sans Mono" font-size="7.5314" lengthAdjust="spacingAndGlyphs" textLength="47.3401" x="130.1853" y="179.6369">checks both</text><!--MD5=[58befbd82e70776cbcefaf9d91600c8d]
|
|
link Verify to Probe--><path d="M115.1871,240.8159 C220.1261,245.5123 447.208,255.6689 559.3933,260.688 " fill="none" id="Verify->Probe" style="stroke: #607985; stroke-width: 0.6993424985056784;"/><polygon fill="#607985" points="562.0293,260.8063,557.291,258.4357,559.3423,260.6835,557.0945,262.7348,562.0293,260.8063" style="stroke: #607985; stroke-width: 0.6993424985056784;"/><text fill="#425B67" font-family="DejaVu Sans Mono" font-size="7.5314" lengthAdjust="spacingAndGlyphs" textLength="98.9839" x="229.1692" y="239.1349">checks preemption proof</text><!--MD5=[544ef8bcaf0d67d3a948fb6a2c2ba12b]
|
|
@startuml
|
|
skinparam backgroundColor white
|
|
skinparam shadowing false
|
|
skinparam monochrome false
|
|
skinparam defaultFontName "DejaVu Sans Mono"
|
|
skinparam defaultFontSize 14
|
|
skinparam defaultFontColor #24343D
|
|
skinparam titleFontName "DejaVu Sans Mono"
|
|
skinparam titleFontSize 13
|
|
skinparam titleFontColor #536B78
|
|
skinparam titleFontStyle plain
|
|
|
|
skinparam ArrowColor #607985
|
|
skinparam ArrowFontColor #425B67
|
|
skinparam ArrowThickness 1.3
|
|
skinparam LineThickness 1.3
|
|
skinparam nodesep 36
|
|
skinparam ranksep 42
|
|
skinparam Padding 6
|
|
|
|
skinparam classBackgroundColor #F5F8FA
|
|
skinparam classBorderColor #607985
|
|
skinparam classBorderThickness 1.5
|
|
skinparam classFontColor #1F3039
|
|
skinparam classFontSize 15
|
|
skinparam classAttributeFontColor #2E424D
|
|
skinparam classAttributeFontSize 13
|
|
skinparam classStereotypeFontColor #526B77
|
|
skinparam classStereotypeFontSize 11
|
|
skinparam minClassWidth 190
|
|
skinparam ClassAttributeIconSize 0
|
|
|
|
skinparam stateBackgroundColor #F5F8FA
|
|
skinparam stateBorderColor #607985
|
|
skinparam stateBorderThickness 1.5
|
|
skinparam stateFontColor #1F3039
|
|
skinparam stateFontSize 14
|
|
skinparam stateAttributeFontSize 13
|
|
|
|
skinparam noteBackgroundColor #F7F5ED
|
|
skinparam noteBorderColor #8A887C
|
|
skinparam noteFontColor #3E4B50
|
|
skinparam noteFontSize 12
|
|
|
|
skinparam ParticipantBackgroundColor #F5F8FA
|
|
skinparam ParticipantBorderColor #607985
|
|
skinparam ParticipantBorderThickness 1.5
|
|
skinparam ParticipantFontColor #1F3039
|
|
skinparam ParticipantFontSize 13
|
|
skinparam ActorBorderColor #607985
|
|
skinparam ActorFontColor #1F3039
|
|
skinparam LifeLineBorderColor #8297A1
|
|
skinparam LifeLineBackgroundColor #F9FBFC
|
|
skinparam SequenceArrowColor #607985
|
|
skinparam SequenceMessageAlign center
|
|
skinparam ParticipantPadding 18
|
|
skinparam BoxPadding 8
|
|
|
|
hide circle
|
|
hide empty members
|
|
scale 900 width
|
|
left to right direction
|
|
|
|
class "01 PeerContext [2]" as Peers <<C struct>> {
|
|
id : uint32_t
|
|
configured_priority : UBaseType_t = 2
|
|
handle : TaskHandle_t
|
|
iterations · checksum
|
|
first_tick · last_tick
|
|
entry_sp · stack range
|
|
}
|
|
|
|
class "02 HighProbeContext" as Probe <<C struct>> {
|
|
initial_priority = 0
|
|
target_priority = 3
|
|
handle : TaskHandle_t
|
|
run_tick
|
|
ran_before_caller_returned
|
|
}
|
|
|
|
class "03 VerifierContext" as Verify <<C struct>> {
|
|
configured_priority = 1
|
|
handle : TaskHandle_t
|
|
pass
|
|
}
|
|
|
|
class "04 switch trace" as SwitchTrace <<bounded record>> {
|
|
task[16]
|
|
tick[16]
|
|
count · changes
|
|
captured A · B · A
|
|
}
|
|
|
|
class "05 preemption markers" as OrderTrace <<bounded record>> {
|
|
1 = before_raise
|
|
2 = high_probe
|
|
3 = after_raise
|
|
}
|
|
|
|
Peers - -> SwitchTrace : one entry per observed task change
|
|
Peers - -> Probe : vTaskPrioritySet(handle, 3)
|
|
Probe - -> OrderTrace : marker 2
|
|
Peers - -> OrderTrace : markers 1 and 3
|
|
Verify - -> Peers : checks both
|
|
Verify - -> Probe : checks preemption proof
|
|
|
|
note bottom of SwitchTrace
|
|
A→B→A is a committed subsequence.
|
|
Repeated loop iterations are not logged.
|
|
end note
|
|
@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> |
