144 lines
17 KiB
XML
144 lines
17 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="338.9189px" preserveAspectRatio="none" style="width:896px;height:338px;" version="1.1" viewBox="0 0 896 338" width="896.2162px" zoomAndPan="magnify"><defs/><g><!--MD5=[7b5bd88a8a025decccf0c9eac4aaabe9]
|
|
class Worker--><rect fill="#F5F8FA" height="172.3184" id="Worker" style="stroke: #607985; stroke-width: 0.8108108108108109;" width="164.3243" x="453.2432" y="4.2"/><text fill="#1F3039" font-family="DejaVu Sans Mono" font-size="8.1081" lengthAdjust="spacingAndGlyphs" textLength="82.7027" x="494.0541" y="17.6721">01 WorkerContext</text><line style="stroke: #607985; stroke-width: 0.8108108108108109;" x1="453.7838" x2="617.027" y1="25.5302" y2="25.5302"/><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="60.5405" x="459.7297" y="37.4583">+id : uint32_t</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="116.7568" x="459.7297" y="52.1247">+result : volatile uint32_t</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="134.0541" x="459.7297" y="66.7911">+iterations : volatile uint32_t</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="134.0541" x="459.7297" y="81.4574">+trace_state : WorkerTraceState</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="108.1081" x="459.7297" y="96.1238">+02 handle : TaskHandle_t</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="116.7568" x="459.7297" y="110.7902">+created_handle : uintptr_t</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="151.3514" x="459.7297" y="125.4566">+start_tick / end_tick : TickType_t</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="103.7838" x="459.7297" y="140.123">+tcb_address : uintptr_t</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="151.3514" x="459.7297" y="154.7894">+stack_low / stack_high : uintptr_t</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="90.8108" x="459.7297" y="169.4558">+entry_sp : uintptr_t</text><!--MD5=[e0ad55b29637cf127d65177e32583e01]
|
|
class Contexts--><rect fill="#F5F8FA" height="83.0617" id="Contexts" style="stroke: #607985; stroke-width: 0.8108108108108109;" width="125.4054" x="228.1081" y="10.4541"/><text fill="#526B77" font-family="DejaVu Sans Mono" font-size="5.9459" font-style="italic" lengthAdjust="spacingAndGlyphs" textLength="22.7027" x="279.4595" y="21.9192">«data»</text><text fill="#1F3039" font-family="DejaVu Sans Mono" font-size="8.1081" lengthAdjust="spacingAndGlyphs" textLength="92.4324" x="244.5946" y="37.3341">03 static contexts</text><line style="stroke: #607985; stroke-width: 0.8108108108108109;" x1="228.6486" x2="352.973" y1="45.1922" y2="45.1922"/><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="112.4324" x="234.5946" y="57.1203">g_worker_a : WorkerContext</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="112.4324" x="234.5946" y="71.7867">g_worker_b : WorkerContext</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="103.7838" x="234.5946" y="86.4531">lifetime = whole program</text><!--MD5=[d356c8aee395c51644a6e46295a3cd9b]
|
|
class Entries--><rect fill="#F5F8FA" height="83.0617" id="Entries" style="stroke: #607985; stroke-width: 0.8108108108108109;" width="138.3784" x="3.2432" y="128.2919"/><text fill="#526B77" font-family="DejaVu Sans Mono" font-size="5.9459" font-style="italic" lengthAdjust="spacingAndGlyphs" textLength="26.4865" x="59.1892" y="139.757">«C ABI»</text><text fill="#1F3039" font-family="DejaVu Sans Mono" font-size="8.1081" lengthAdjust="spacingAndGlyphs" textLength="102.1622" x="21.3514" y="155.1719">04 C entry functions</text><line style="stroke: #607985; stroke-width: 0.8108108108108109;" x1="3.7838" x2="141.0811" y1="163.0301" y2="163.0301"/><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="90.8108" x="9.7297" y="174.9581">sum_task_entry(void*)</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="121.0811" x="9.7297" y="189.6245">supervisor_task_entry(void*)</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="125.4054" x="9.7297" y="204.2909">create_worker(WorkerContext*)</text><!--MD5=[4f126f465601d391fe0c3c00f8b450b3]
|
|
class Supervisor--><rect fill="#F5F8FA" height="84.3201" id="Supervisor" style="stroke: #607985; stroke-width: 0.8108108108108109;" width="116.7568" x="232.4324" y="168.2"/><text fill="#1F3039" font-family="DejaVu Sans Mono" font-size="8.1081" lengthAdjust="spacingAndGlyphs" textLength="102.1622" x="239.7297" y="181.6721">05 SupervisorContext</text><line style="stroke: #607985; stroke-width: 0.8108108108108109;" x1="232.973" x2="348.6486" y1="189.5302" y2="189.5302"/><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="95.1351" x="238.9189" y="201.4583">first : WorkerContext*</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="99.4595" x="238.9189" y="216.1247">second : WorkerContext*</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="90.8108" x="238.9189" y="230.7911">handle : TaskHandle_t</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="103.7838" x="238.9189" y="245.4574">pass : volatile uint32_t</text><!--MD5=[3c1aae6a6af91a00aebe86d2dd4d752e]
|
|
class Invariants--><rect fill="#F5F8FA" height="83.0617" id="Invariants" style="stroke: #607985; stroke-width: 0.8108108108108109;" width="164.3243" x="453.2432" y="249.9135"/><text fill="#526B77" font-family="DejaVu Sans Mono" font-size="5.9459" font-style="italic" lengthAdjust="spacingAndGlyphs" textLength="37.8378" x="516.4865" y="261.3786">«contract»</text><text fill="#1F3039" font-family="DejaVu Sans Mono" font-size="8.1081" lengthAdjust="spacingAndGlyphs" textLength="102.1622" x="484.3243" y="276.7935">06 common invariants</text><line style="stroke: #607985; stroke-width: 0.8108108108108109;" x1="453.7838" x2="617.027" y1="284.6517" y2="284.6517"/><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="134.0541" x="459.7297" y="296.5797">result A = result B = 200010000</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="151.3514" x="459.7297" y="311.2461">iterations A = iterations B = 20000</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="112.4324" x="459.7297" y="325.9125">trace contains A -> B -> A</text><!--MD5=[e9f17e4922be6079066fa450c8bff6eb]
|
|
class Heap--><rect fill="#F5F8FA" height="83.0617" id="Heap" style="stroke: #607985; stroke-width: 0.8108108108108109;" width="108.1081" x="782.1622" y="48.8324"/><text fill="#526B77" font-family="DejaVu Sans Mono" font-size="5.9459" font-style="italic" lengthAdjust="spacingAndGlyphs" textLength="34.0541" x="819.1892" y="60.2975">«runtime»</text><text fill="#1F3039" font-family="DejaVu Sans Mono" font-size="8.1081" lengthAdjust="spacingAndGlyphs" textLength="29.1892" x="821.6216" y="75.7124">heap_4</text><line style="stroke: #607985; stroke-width: 0.8108108108108109;" x1="782.7027" x2="889.7297" y1="83.5706" y2="83.5706"/><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="56.2162" x="788.6486" y="95.4987">TCB A / TCB B</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="73.5135" x="788.6486" y="110.165">stack A / stack B</text><text fill="#2E424D" font-family="DejaVu Sans Mono" font-size="7.027" lengthAdjust="spacingAndGlyphs" textLength="95.1351" x="788.6486" y="124.8314">supervisor TCB + stack</text><path d="M435.6757,195.7892 L435.6757,230.3331 A0,0 0 0 0 435.6757,230.3331 L635.1351,230.3331 A0,0 0 0 0 635.1351,230.3331 L635.1351,201.1946 L629.7297,195.7892 L537.5676,195.7892 L535.4054,176.6649 L533.2432,195.7892 L435.6757,195.7892 A0,0 0 0 0 435.6757,195.7892 " fill="#F7F5ED" style="stroke: #8A887C; stroke-width: 0.5405405405405406;"/><path d="M629.7297,195.7892 L629.7297,201.1946 L635.1351,201.1946 L629.7297,195.7892 " fill="#F7F5ED" style="stroke: #8A887C; stroke-width: 0.5405405405405406;"/><text fill="#3E4B50" font-family="DejaVu Sans Mono" font-size="6.4865" lengthAdjust="spacingAndGlyphs" textLength="140" x="442.1622" y="207.756">Context is application-owned storage.</text><text fill="#3E4B50" font-family="DejaVu Sans Mono" font-size="6.4865" lengthAdjust="spacingAndGlyphs" textLength="181.6216" x="442.1622" y="215.3067">&handle is a field address; handle is its value.</text><text fill="#3E4B50" font-family="DejaVu Sans Mono" font-size="6.4865" lengthAdjust="spacingAndGlyphs" textLength="155.1351" x="442.1622" y="222.8574">Neither is the separate task-stack block.</text><!--MD5=[77eb6e05bec067ba2b628dcc54dd7b08]
|
|
reverse link Contexts to Worker--><path d="M361.4919,63.0378 C390.1027,67.5459 423.3838,72.7892 453.0919,77.4757 " fill="none" id="Contexts<-Worker" style="stroke: #607985; stroke-width: 0.7027027027027027;"/><polygon fill="#607985" points="354.5568,61.9459,357.4254,64.585,360.9647,62.9521,358.0961,60.313,354.5568,61.9459" style="stroke: #607985; stroke-width: 0.7027027027027027;"/><text fill="#425B67" font-family="DejaVu Sans Mono" font-size="7.5676" lengthAdjust="spacingAndGlyphs" textLength="51.8919" x="368.6486" y="58.9865">contains two</text><!--MD5=[0a09065219b8fc4c2741fad6d91ed526]
|
|
reverse link Supervisor to Worker--><path d="M356.7297,188.9838 C378.6324,181.0162 402.9189,171.2919 424.3243,160.6324 C433.8432,155.8919 443.5676,150.5405 453.1135,144.9568 " fill="none" id="Supervisor<-Worker" style="stroke: #607985; stroke-width: 0.7027027027027027;"/><polygon fill="#FFFFFF" points="350.173,191.3405,353.9557,192.2809,356.2787,189.1508,352.4959,188.2104,350.173,191.3405" style="stroke: #607985; stroke-width: 0.7027027027027027;"/><text fill="#425B67" font-family="DejaVu Sans Mono" font-size="7.5676" lengthAdjust="spacingAndGlyphs" textLength="34.5946" x="377.2973" y="155.2244">observes</text><!--MD5=[2c6bfd4e3ad4845782e2d985564dafc6]
|
|
link Entries to Worker--><path d="M141.8757,157.9676 C223.9351,143.8486 361.0162,120.2703 449.6595,105.0162 " fill="none" id="Entries->Worker" style="stroke: #607985; stroke-width: 0.7027027027027027;"/><polygon fill="#607985" points="452.2486,104.573,447.0889,103.2618,449.5846,105.0286,447.8179,107.5243,452.2486,104.573" style="stroke: #607985; stroke-width: 0.7027027027027027;"/><text fill="#425B67" font-family="DejaVu Sans Mono" font-size="7.5676" lengthAdjust="spacingAndGlyphs" textLength="56.2162" x="262.7027" y="116.7865">typed context</text><!--MD5=[f79e6be81bdb53c12d9f736eae846aaf]
|
|
link Entries to Supervisor--><path d="M141.8757,182.6757 C169.773,187.8811 201.7189,193.8378 228.8108,198.8973 " fill="none" id="Entries->Supervisor" style="stroke: #607985; stroke-width: 0.7027027027027027;"/><polygon fill="#607985" points="231.4541,199.3892,227.0752,196.3614,228.7983,198.8874,226.2723,200.6105,231.4541,199.3892" style="stroke: #607985; stroke-width: 0.7027027027027027;"/><text fill="#425B67" font-family="DejaVu Sans Mono" font-size="7.5676" lengthAdjust="spacingAndGlyphs" textLength="56.2162" x="156.7568" y="179.8568">typed context</text><!--MD5=[50e4ee6a0204c339eccdd06d48720435]
|
|
link Worker to Heap--><path d="M617.6486,90.3622 C668.5838,90.3622 732.8703,90.3622 778.4,90.3622 " fill="none" id="Worker->Heap" style="stroke: #607985; stroke-width: 0.7027027027027027;"/><polygon fill="#607985" points="781.1027,90.3622,776.2378,88.2,778.4,90.3622,776.2378,92.5243,781.1027,90.3622" style="stroke: #607985; stroke-width: 0.7027027027027027;"/><text fill="#425B67" font-family="DejaVu Sans Mono" font-size="7.5676" lengthAdjust="spacingAndGlyphs" textLength="116.7568" x="650.2703" y="84.9541">handle value identifies TCB</text><!--MD5=[b5aa81ced6422ec50f89e7cce099c4d3]
|
|
link Supervisor to Invariants--><path d="M349.3676,229.6811 C379.4216,239.6865 416.6811,252.0919 449.9081,263.1568 " fill="none" id="Supervisor->Invariants" style="stroke: #607985; stroke-width: 0.7027027027027027;"/><polygon fill="#607985" points="452.3351,263.9622,448.3972,260.3797,449.7696,263.1121,447.0371,264.4845,452.3351,263.9622" style="stroke: #607985; stroke-width: 0.7027027027027027;"/><text fill="#425B67" font-family="DejaVu Sans Mono" font-size="7.5676" lengthAdjust="spacingAndGlyphs" textLength="34.5946" x="377.2973" y="231.1811">verifies</text><!--MD5=[bd196756b6337a178e85cd39afe76fb8]
|
|
@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 WorkerContext" as Worker {
|
|
+id : uint32_t
|
|
+result : volatile uint32_t
|
|
+iterations : volatile uint32_t
|
|
+trace_state : WorkerTraceState
|
|
+02 handle : TaskHandle_t
|
|
+created_handle : uintptr_t
|
|
+start_tick / end_tick : TickType_t
|
|
+tcb_address : uintptr_t
|
|
+stack_low / stack_high : uintptr_t
|
|
+entry_sp : uintptr_t
|
|
}
|
|
|
|
class "03 static contexts" as Contexts <<data>> {
|
|
g_worker_a : WorkerContext
|
|
g_worker_b : WorkerContext
|
|
lifetime = whole program
|
|
}
|
|
|
|
class "04 C entry functions" as Entries <<C ABI>> {
|
|
sum_task_entry(void*)
|
|
supervisor_task_entry(void*)
|
|
create_worker(WorkerContext*)
|
|
}
|
|
|
|
class "05 SupervisorContext" as Supervisor {
|
|
first : WorkerContext*
|
|
second : WorkerContext*
|
|
handle : TaskHandle_t
|
|
pass : volatile uint32_t
|
|
}
|
|
|
|
class "06 common invariants" as Invariants <<contract>> {
|
|
result A = result B = 200010000
|
|
iterations A = iterations B = 20000
|
|
trace contains A -> B -> A
|
|
}
|
|
|
|
class "heap_4" as Heap <<runtime>> {
|
|
TCB A / TCB B
|
|
stack A / stack B
|
|
supervisor TCB + stack
|
|
}
|
|
|
|
Contexts *- - Worker : contains two
|
|
Supervisor o- - Worker : observes
|
|
Entries - -> Worker : typed context
|
|
Entries - -> Supervisor : typed context
|
|
Worker - -> Heap : handle value identifies TCB
|
|
Supervisor - -> Invariants : verifies
|
|
|
|
note bottom of Worker
|
|
Context is application-owned storage.
|
|
&handle is a field address; handle is its value.
|
|
Neither is the separate task-stack block.
|
|
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> |
