*{box-sizing:border-box}body{margin:0}var,address{font-style:normal}fieldset{margin-inline:0;padding-block:0;padding-inline:0;border:none}:root{--font-size: 21px;--font-color: black;--muted-font-color: grey;--link-color: blue;--background-color: rgb(255, 246, 229);--highlight-color: rgb(9, 255, 0);--clock-drift-color: blue;--font-family: NewComputerModern10, serif;--math-font-family: NewComputerModernMath}@media (prefers-color-scheme: dark){:root{--font-color: white;--muted-font-color: #ccc;--link-color: #9b9bff;--background-color: black;--clock-drift-color: lightblue}}@media (width <=520px){:root{--font-size: 18px}}:root{font-size:var(--font-size);font-family:var(--font-family)}body{color:var(--font-color);background-color:var(--background-color)}body{display:grid;grid-template-areas:". article ." ". footer .";grid-template-columns:1fr auto 1fr}body>article{grid-area:article}body>footer{grid-area:footer}article{max-width:35em}address{display:flex;flex-direction:column}address{margin-bottom:1em}section#copyright{font-size:.5em}article>header{font-weight:700;font-size:2em}article>header{margin-bottom:.5em}article>section>header{font-size:1.5em;font-weight:700}article>section>section>header{font-size:1em;font-weight:700}figure{display:flex;flex-direction:column;align-items:center;max-width:20em;margin-left:auto;margin-right:auto}span.link,span[data-process]{text-decoration:underline dotted}a,a[href^="#"]:visited{color:var(--link-color)}span.summary{text-decoration:underline dotted;cursor:pointer}span.summary:before{content:"▸"}span.summary.open:before{content:"▾"}div.arrow{display:none;position:absolute;top:-1.5em;width:1em;height:1em;border-left:solid 1em transparent;border-right:solid 1em transparent;border-bottom:solid 1em black}div.arrow.open{display:block}div.arrow:after{content:"";width:0;height:0;border-left:solid 1em transparent;border-right:solid 1em transparent;border-bottom:solid 1em var(--background-color);position:absolute;top:2px;left:-1em}div.details{display:none;margin-top:.5em;border-radius:.25em;border:solid black 2px;padding:.5em;box-shadow:inset .125em .125em .25em 0 var(--muted-font-color)}div.details.open{display:block}details>summary{text-decoration:dotted underline;cursor:pointer}ol.visual,ul.visual{list-style:none;margin-block-start:0;margin-block-end:0;padding-inline:0;display:grid;grid-template-columns:repeat(auto-fit,minmax(15em,1fr));column-gap:1em}:is(ol.visual,ul.visual) li{display:grid;grid-template-rows:subgrid;grid-template-columns:subgrid;grid-column:span 1;grid-row:span 2;justify-content:center;justify-items:center;flex-basis:10em;flex-grow:1}:is(ol.visual,ul.visual) p,:is(ol.visual,ul.visual) figure{margin:0}ul.visual.example{list-style:none;display:flex;flex-direction:row;flex-wrap:wrap;justify-content:space-evenly}ul.visual.example>li{flex-basis:10em}ol.implementation-rule{padding-inline-start:3em}ol.implementation-rule>li::marker{content:"IR" counter(list-item) ". "}ol#clock-condition-list>li::marker{content:"C" counter(list-item) ". "}ol.physical-clock{padding-inline-start:3em}ol.physical-clock>li::marker{content:"PC" counter(list-item) ". ";font-weight:700}ol#physical-implementation-rules{padding-inline-start:5em}ol#physical-implementation-rules>li::marker{content:"IR" counter(list-item) "'. "}button[popovertarget]{font-family:var(--font-family);cursor:pointer}dialog{border:solid black 2px;border-radius:.5em;padding:1em;max-width:min(30em,100vw);max-height:80vh;overflow-y:auto;color:var(--font-color);background-color:var(--background-color)}dialog::backdrop{background:#0006}li>template-use{display:block}ul.visual svg.space-time,ul.visual space-time{width:10em}ol.visual svg.distributed-system{width:10em}ol.visual directed-graph{width:10em}#implementation-rule-2>figure{display:flex;flex-direction:row;justify-content:center;max-width:none}:is(#implementation-rule-2>figure)>space-time{max-width:15em}:is(#implementation-rule-2>figure)>form{display:flex;flex-direction:column;align-items:center;row-gap:.5em}#total-ordering-simulation{row-gap:.5em}.reference .book.title,.reference .journal,.reference .volume{font-style:italic}footer#feedback{display:flex;flex-direction:row;justify-content:space-between}a.icon{display:inline-flex;flex-direction:row;align-items:center;column-gap:.25em}a.icon:before{content:" ";display:inline-block;background-position:center;background-repeat:no-repeat;background-size:contain;width:1em;height:1em}a.icon[href^="https://github.com/"]:before{background-image:url("data:image/svg+xml,%3csvg%20width='98'%20height='96'%20xmlns='http://www.w3.org/2000/svg'%3e%3cpath%20fill-rule='evenodd'%20clip-rule='evenodd'%20d='M48.854%200C21.839%200%200%2022%200%2049.217c0%2021.756%2013.993%2040.172%2033.405%2046.69%202.427.49%203.316-1.059%203.316-2.362%200-1.141-.08-5.052-.08-9.127-13.59%202.934-16.42-5.867-16.42-5.867-2.184-5.704-5.42-7.17-5.42-7.17-4.448-3.015.324-3.015.324-3.015%204.934.326%207.523%205.052%207.523%205.052%204.367%207.496%2011.404%205.378%2014.235%204.074.404-3.178%201.699-5.378%203.074-6.6-10.839-1.141-22.243-5.378-22.243-24.283%200-5.378%201.94-9.778%205.014-13.2-.485-1.222-2.184-6.275.486-13.038%200%200%204.125-1.304%2013.426%205.052a46.97%2046.97%200%200%201%2012.214-1.63c4.125%200%208.33.571%2012.213%201.63%209.302-6.356%2013.427-5.052%2013.427-5.052%202.67%206.763.97%2011.816.485%2013.038%203.155%203.422%205.015%207.822%205.015%2013.2%200%2018.905-11.404%2023.06-22.324%2024.283%201.78%201.548%203.316%204.481%203.316%209.126%200%206.6-.08%2011.897-.08%2013.526%200%201.304.89%202.853%203.316%202.364%2019.412-6.52%2033.405-24.935%2033.405-46.691C97.707%2022%2075.788%200%2048.854%200z'%20fill='%2324292f'/%3e%3c/svg%3e")}@media (prefers-color-scheme: dark){a.icon[href^="https://github.com/"]:before{background-image:url("data:image/svg+xml,%3csvg%20width='98'%20height='96'%20xmlns='http://www.w3.org/2000/svg'%3e%3cpath%20fill-rule='evenodd'%20clip-rule='evenodd'%20d='M48.854%200C21.839%200%200%2022%200%2049.217c0%2021.756%2013.993%2040.172%2033.405%2046.69%202.427.49%203.316-1.059%203.316-2.362%200-1.141-.08-5.052-.08-9.127-13.59%202.934-16.42-5.867-16.42-5.867-2.184-5.704-5.42-7.17-5.42-7.17-4.448-3.015.324-3.015.324-3.015%204.934.326%207.523%205.052%207.523%205.052%204.367%207.496%2011.404%205.378%2014.235%204.074.404-3.178%201.699-5.378%203.074-6.6-10.839-1.141-22.243-5.378-22.243-24.283%200-5.378%201.94-9.778%205.014-13.2-.485-1.222-2.184-6.275.486-13.038%200%200%204.125-1.304%2013.426%205.052a46.97%2046.97%200%200%201%2012.214-1.63c4.125%200%208.33.571%2012.213%201.63%209.302-6.356%2013.427-5.052%2013.427-5.052%202.67%206.763.97%2011.816.485%2013.038%203.155%203.422%205.015%207.822%205.015%2013.2%200%2018.905-11.404%2023.06-22.324%2024.283%201.78%201.548%203.316%204.481%203.316%209.126%200%206.6-.08%2011.897-.08%2013.526%200%201.304.89%202.853%203.316%202.364%2019.412-6.52%2033.405-24.935%2033.405-46.691C97.707%2022%2075.788%200%2048.854%200z'%20fill='%23fff'/%3e%3c/svg%3e")}}template-use{width:100%;height:100%}#implementation-rule-2a-controls{display:flex;flex-direction:row;column-gap:.5em}#implementation-rule-2b-controls{display:flex;flex-direction:row;column-gap:1em}#implementation-rule-2b-controls>fieldset{min-inline-size:auto;display:flex;flex-direction:column;row-gap:.5em}button{border:solid 2px var(--font-color);border-radius:.25em;padding:.25em;font-family:var(--font-family);font-size:1em;background-color:transparent;box-shadow:2px 2px 1px 1px var(--muted-font-color);margin:0 3px 3px 0}button:not(:disabled):hover{cursor:pointer;box-shadow:2px 2px 1px 1px var(--font-color)}button:not(:disabled):active{box-shadow:inset 1px 1px 1px 1px var(--font-color)}button:disabled{border-color:var(--muted-font-color)}fieldset{border-color:var(--muted-font-color)}figure#physical-clock-example,figure#physical-clock-speed-error,figure#physical-clock-system{display:flex;flex-direction:column;align-items:center}:is(figure#physical-clock-example,figure#physical-clock-speed-error,figure#physical-clock-system)>form{display:flex;flex-direction:column;row-gap:.25em;align-items:center}figure#physical-clock-system{--timestamp-color: lightgrey;--min-future-color: blue;--current-color: var(--highlight-color)}figure#real-clock-theorem{display:flex;flex-direction:column;align-items:center}#real-clock-theorem>section:first-of-type{display:flex;flex-direction:column;align-items:center}:is(#real-clock-theorem>section:first-of-type)>form{display:flex;flex-direction:row;column-gap:1em;align-items:baseline}form label.variable{display:flex;flex-direction:row}form label.variable.range{display:grid;grid-template-areas:"math input";grid-template-columns:auto 1fr;column-gap:.5em}label.variable>math{min-width:max-content}figure#minimal-causal-delay-diagram{max-width:12em}fieldset.variable{display:grid;grid-template-columns:auto 1fr;row-gap:.25em}fieldset.variable label.variable.range{grid-column:span 2;display:grid;grid-template-columns:subgrid}fieldset{border:2px solid var(--font-color);border-radius:.25em;padding:.5em}fieldset.time{display:flex;flex-direction:row;flex-wrap:nowrap;align-items:baseline;justify-content:center;column-gap:.25em}figure#physical-clock-system>form{display:grid;grid-template-areas:"clock-1 message clock-2" ". time ." ". reset .";column-gap:.5em;row-gap:.5em;align-items:center}:is(figure#physical-clock-system>form)>fieldset[name="clock 1"]{grid-area:clock-1}:is(figure#physical-clock-system>form)>fieldset[name="clock 2"]{grid-area:clock-2}:is(figure#physical-clock-system>form)>fieldset[name=message]{grid-area:message}:is(figure#physical-clock-system>form)>fieldset.time{grid-area:time}:is(figure#physical-clock-system>form)>button[type=reset]{grid-area:reset}fieldset.clock{display:flex;flex-direction:column;flex-wrap:nowrap;row-gap:.25em}@media (width <=65em){figure#physical-clock-system>form{grid-template-areas:"clock-1" "message" "clock-2" "time" "reset"}}#physical-clock-simple-system form{display:grid;grid-template-areas:"lhs lhs   rhs   rhs" ".   err   err   ." ".   time  time  ." ".   reset reset .";row-gap:.5em;column-gap:.5em}:is(#physical-clock-simple-system form)>fieldset:nth-of-type(1){grid-area:lhs}:is(#physical-clock-simple-system form)>fieldset:nth-of-type(2){grid-area:rhs}:is(#physical-clock-simple-system form)>fieldset.time{grid-area:time}:is(#physical-clock-simple-system form)>label{grid-area:err}:is(#physical-clock-simple-system form) button[type=reset]{grid-area:reset}@media (width <=65em){#physical-clock-simple-system>form{grid-template-areas:"lhs" "rhs" "err" "time" "reset"}}figure#real-clock-theorem{display:grid;grid-template-areas:"graph chart" "graph controls" "caption  caption";align-items:center;justify-content:center;justify-items:center;row-gap:.5em;column-gap:.5em}figure#real-clock-theorem>section:nth-of-type(1){grid-area:graph}figure#real-clock-theorem>figcaption{grid-area:caption}figure#real-clock-theorem>form{grid-area:controls}figure#real-clock-theorem #real-clock-theorem-drift{grid-area:chart}figure#real-clock-theorem form{display:flex;flex-direction:column;row-gap:.25em;align-items:center}@media (width <=60em){figure#real-clock-theorem{grid-template-areas:"graph" "chart" "controls" "caption"}}section.equation{display:flex;flex-direction:row;align-items:center;margin:1em 0}section.equation>math{flex-grow:1;margin:0;justify-self:center;math-style:normal}ol.math.derivation{list-style:none;display:grid;grid-template-columns:[lhs] auto [rhs] auto [reason] auto;align-items:baseline;row-gap:.25em}ol.math.derivation>li{display:contents}:is(ol.math.derivation>li):first-child>math:first-of-type{grid-column:lhs}:is(ol.math.derivation>li)>math{grid-column-start:rhs;justify-self:flex-start;math-style:normal}:is(ol.math.derivation>li)>.reason{grid-column:reason}ol.math.derivation math[display=block]{margin:0}math mrow[title],math mi[title],math mo[title],math msub[title],math msup[title],math munder[title],math msubsup[title],math mfrac[title],math mtext.description{cursor:pointer;padding:2px;margin:4px;border-radius:.25em;box-shadow:1px 1px 1px 1px var(--muted-font-color)}:is(math mrow[title],math mi[title],math mo[title],math msub[title],math msup[title],math munder[title],math msubsup[title],math mfrac[title],math mtext.description):hover{box-shadow:1px 1px 1px 1px var(--font-color)}:is(math mrow[title],math mi[title],math mo[title],math msub[title],math msup[title],math munder[title],math msubsup[title],math mfrac[title],math mtext.description):hover:has(mi[title]:hover),:is(math mrow[title],math mi[title],math mo[title],math msub[title],math msup[title],math munder[title],math msubsup[title],math mfrac[title],math mtext.description):hover:has(mrow[title]:hover),:is(math mrow[title],math mi[title],math mo[title],math msub[title],math msup[title],math munder[title],math msubsup[title],math mfrac[title],math mtext.description):hover:has(mo[title]:hover),:is(math mrow[title],math mi[title],math mo[title],math msub[title],math msup[title],math munder[title],math msubsup[title],math mfrac[title],math mtext.description):hover:has(mfrac[title]:hover),:is(math mrow[title],math mi[title],math mo[title],math msub[title],math msup[title],math munder[title],math msubsup[title],math mfrac[title],math mtext.description):hover:has(mtext.description:hover),:is(math mrow[title],math mi[title],math mo[title],math msub[title],math msup[title],math munder[title],math msubsup[title],math mfrac[title],math mtext.description):hover:has(msub[title]:hover){box-shadow:1px 1px 1px 1px var(--muted-font-color)}:is(math mrow[title],math mi[title],math mo[title],math msub[title],math msup[title],math munder[title],math msubsup[title],math mfrac[title],math mtext.description):active{box-shadow:inset 1px 1px 1px 1px var(--font-color)}mtext.description{font-family:var(--font-family)}mtext.separator{margin-left:.5em;margin-right:.5em}mi.set{font-variant-alternates:stylistic(calligraphic);font-feature-settings:"ss01";-webkit-font-feature-settings:"ss01"}mi.underline{text-decoration:underline}msub>mtext:nth-child(2){font-size:.7rem}figure.space-time svg,svg.space-time{max-width:20em;max-height:20em}:is(figure.space-time svg,svg.space-time) g.process line.segment{stroke:var(--font-color)}.highlight:is(:is(figure.space-time svg,svg.space-time) g.process line.segment){stroke:var(--highlight-color)}:is(:is(figure.space-time svg,svg.space-time) g.process line.segment):last-of-type{marker-end:url(#arrow)}:is(figure.space-time svg,svg.space-time) g.process line.segment:last-of-type{marker-end:url(#arrow)}:is(figure.space-time svg,svg.space-time) g.message line{stroke:var(--font-color);stroke-width:1;fill:none;marker-end:url(#message)}:is(figure.space-time svg,svg.space-time) g.message.receive line{marker-start:url(#message);marker-end:url(#arrow)}:is(figure.space-time svg,svg.space-time) g.tick polyline{stroke:var(--font-color);stroke-width:1;stroke-dasharray:2 2}:is(figure.space-time svg,svg.space-time) line.tick{stroke-dasharray:2 2}:is(figure.space-time svg,svg.space-time) polyline.period{fill:none;stroke:var(--font-color)}:is(figure.space-time svg,svg.space-time) polyline.tick{stroke:var(--font-color);stroke-width:1;stroke-dasharray:2 2;fill:none}:is(:is(:is(figure.space-time svg,svg.space-time) g.process.highlight) g.event) circle{fill:var(--highlight-color)}:is(:is(figure.space-time svg,svg.space-time) g.process.highlight) line.segment{stroke:var(--highlight-color)}:is(:is(figure.space-time svg,svg.space-time) g.event.ghost) circle{fill:var(--background-color);stroke:var(--font-color)}:is(:is(figure.space-time svg,svg.space-time) g.event) circle{fill:var(--font-color)}.highlight:is(:is(figure.space-time svg,svg.space-time) g.event) circle{fill:var(--highlight-color)}:is(:is(figure.space-time svg,svg.space-time) g.message.highlight) path{stroke:var(--highlight-color)}.link:is(:is(:is(figure.space-time svg,svg.space-time) g.message.highlight) path){marker-end:url(#arrow-highlight)}:is(:is(:is(figure.space-time svg,svg.space-time) defs) marker#arrow) *{stroke-width:0;stroke:var(--font-color);fill:var(--font-color)}:is(:is(:is(figure.space-time svg,svg.space-time) defs) marker#arrow-highlight) *{stroke-width:0;fill:var(--highlight-color)}:is(figure.space-time svg,svg.space-time) text{font-size:.3em;fill:var(--font-color)}.highlight:is(:is(figure.space-time svg,svg.space-time) text){fill:var(--highlight-color)}:is(figure.space-time svg,svg.space-time) path{stroke:var(--font-color)}.highlight:is(:is(figure.space-time svg,svg.space-time) path){stroke:var(--highlight-color)}.message:is(:is(figure.space-time svg,svg.space-time) path){fill:none;marker-end:url(#arrow)}.message.highlight:is(:is(figure.space-time svg,svg.space-time) path){marker-end:url(#arrow-highlight)}.link:is(:is(figure.space-time svg,svg.space-time) path){fill:none;marker-end:url(#arrow)}.link.highlight:is(:is(figure.space-time svg,svg.space-time) path){marker-end:url(#arrow-highlight)}:is(figure.space-time svg,svg.space-time) foreignObject.label{color:var(--font-color);font-size:6px}:is(:is(figure.space-time svg,svg.space-time) foreignObject.label) msub>:not(:first-child){font-size:4px}.selection:is(figure.space-time svg,svg.space-time) circle.event{cursor:pointer}:is(:is(figure.space-time svg,svg.space-time) g.message)>g.icon>path{fill:var(--background-color);stroke-width:1;stroke:var(--font-color);stroke-linecap:round;stroke-linejoin:round}:is(:is(figure.space-time svg,svg.space-time) g.message)>path{fill:var(--background-color);stroke-width:1;stroke:var(--font-color);stroke-linecap:round;stroke-linejoin:round}:is(figure.space-time svg,svg.space-time) line.link{fill:none;stroke-width:1;stroke:var(--font-color);stroke-dasharray:4 4}:is(:is(:is(figure.space-time svg,svg.space-time) g.event) circle):hover{fill:var(--highlight-color)}.selectable:is(figure.space-time svg,svg.space-time) g.event circle:hover{cursor:pointer}:is(:is(svg.distributed-system defs) #message,:is(svg.distributed-system defs) #message-reverse) rect{fill:var(--background-color);stroke:var(--font-color);stroke-width:1}:is(:is(svg.distributed-system defs) #message,:is(svg.distributed-system defs) #message-reverse) path{fill:var(--background-color);stroke:var(--font-color);stroke-width:1}:is(svg.distributed-system g.process)>circle{fill:var(--background-color);stroke-width:1;stroke:var(--font-color)}:is(svg.distributed-system g.process)>text{fill:var(--font-color);font-size:5px;text-anchor:middle;vertical-align:middle}svg.distributed-system line.link{fill:none;stroke-width:1;stroke:var(--font-color);stroke-dasharray:4 4}svg.distributed-system line.message{fill:none;stroke-width:1;stroke:var(--font-color);marker-end:url(#message)}.reverse:is(svg.distributed-system line.message){marker-end:url(#message-reverse)}:is(svg.distributed-system g.message)>path{fill:var(--background-color);stroke-width:1;stroke:var(--font-color);stroke-linecap:round;stroke-linejoin:round}svg.distributed-system circle.process{stroke-width:2;fill:none;stroke:var(--font-color)}svg line{stroke:var(--font-color)}svg path{stroke:var(--font-color);fill:none}svg circle{fill:var(--font-color)}svg foreignObject{color:var(--font-color);font-size:6px}:is(svg foreignObject) msub>:not(:first-child){font-size:4px}