Profil určuje, jak často má worker vytvářet checkpoint, a zastaralá úloha se hlásí

deklarovaný stav!deklarovaný stav: advisory Promítnuto do instrukcí workera. Zda je worker dodržuje, zvenčí pozorovat nelze. Je to dokumentace, ne vynucování.

zaznamenané důkazy○zaznamenané důkazy: nespuštěno Neposuzováno: k zaznamenanému běhu je vázáno jen zaručené tvrzení. jak se zaznamenávají důkazy

Zpráva o zastaralosti je zaručena. To, zda worker vytváří kontrolní body, zaručeno není.

majordomus check --checkpoint
majordomus watch     # DRIFT staleness … when the interval has passed

Detail vykreslený z docs/claims/checkpoint-interval.md.

Od tvrzení k důkazu

1. 1 · veřejné tvrzení

   Profil určuje, jak často má worker vytvářet checkpoint, a zastaralá úloha se hlásí

   Vytvořeno na Profiles.

2. 2 · kanonické tvrzení

   checkpoint-interval!deklarovaný stav: advisory v docs/CLAIMS.yaml

   Definováno v přečtěte si na tomto webu · share/skeleton/policy.yaml

3. 3 · implementace

   lib/check.sh · majordomus check

4. 4 · test a scénáře

   Test: test/cases/04_start_check.sh

5. 5 · zaznamenané běhy

   ○zaznamenané důkazy: nespuštěno jak se zaznamenávají důkazy

Ověřte si to sami

Test běží v jednorázovém dočasném repozitáři a ověřuje chování, ne řetězec ve zdrojovém kódu.

bash test/run.sh 04_start_check

Kde se toto tvrzení používá

Související tvrzení stejná implementace

• ○deklarovaný stav: zaručeno Každý řádek ledgeru jen pro připojování je dobře utvořená událost a poškozený řádek je selhání, ne přeskočený záznam
• !deklarovaný stav: doporučení Záznam rozhodnutí bez úlohy, hlavy a důvodu se ohlásí a neblokuje
• ○deklarovaný stav: zaručeno Záznam v úložišti otázek, který se nezparsuje, blokuje přijetí přesně jako nevyřešená otázka
• ○deklarovaný stav: zaručeno check hlásí, zda jsou stav, rozsah, blokátory a stáří checkpointu právě teď konzistentní
• ○deklarovaný stav: zaručeno Dotčený soubor mimo uplatněný rozsah je selhání, ne varování
• ○deklarovaný stav: zaručeno Překryv mezi paralelními pracovníky se počítá na uplatněných cestách v obou směrech zahrnutí
• !deklarovaný stav: doporučení Profil určuje, jaký kontext má pracovník načíst, a nic víc
• ○deklarovaný stav: zaručeno Záznam úlohy jmenuje checkout, do kterého patří, a jiný checkout se nikdy nesrovnává s jeho rozsahem
• ○deklarovaný stav: zaručeno Blokující otázka blokuje dál i poté, co je práce předána nové úloze

Okamžiky, na které to odpovídá

• → našel úlohu "in progress", které se tři týdny nikdo nedotkl Stav, který byl napsán, a ne spočítán, platí v okamžiku zápisu a odtud tiše zastarává.
• → přišel o selhání, které pracovník už reprodukoval, protože relace skončila Selhání pozorované uvnitř relace je popsáno v této relaci a nikde jinde, takže další začíná od hlášení, ne od důkazu.