@@ -1572,11 +1572,14 @@ pub struct Saves {
15721572 /// `/data`), and no snapshot is kept until a start comes up.
15731573 #[ serde( default ) ]
15741574 fresh : bool ,
1575- /// Its disk as last read (`measured`): a cache, which a release from
1576- /// before it drops as it writes its saves back (the next start or save
1577- /// reads it again).
1575+ /// Its disk as last read (`measured`), and whether its owner is told it
1576+ /// is filling (a latch: `disk_filling` sets it, `disk_clear` clears it):
1577+ /// a cache, which a release from before it drops as it writes its saves
1578+ /// back (the next read sets both again).
15781579 #[ serde( default ) ]
15791580 disk : Option < ComputerDisk > ,
1581+ #[ serde( default ) ]
1582+ disk_told : bool ,
15801583}
15811584
15821585/// A start that went back in time, as its owner is told of it.
@@ -1866,6 +1869,7 @@ impl Saves {
18661869 if self . disk . is_some_and ( |d| d. at > disk. at ) {
18671870 return false ;
18681871 }
1872+ self . disk_told = if self . disk_told { !disk_clear ( disk. total , disk. free ) } else { disk_filling ( disk. total , disk. free ) } ;
18691873 self . disk = Some ( disk) ;
18701874 true
18711875 }
@@ -2011,6 +2015,14 @@ const _: () = assert!(DISK_TOLD_USED_PCT > 0 && DISK_TOLD_USED_PCT < 100, "told
20112015/// room it has plenty of.
20122016pub const DISK_TOLD_FREE_MAX : u64 = 5_000_000_000 ;
20132017
2018+ /// Told, it is told no more only once a read finds clearly more room:
2019+ /// at most this much used, or at least `DISK_CLEAR_FREE_MIN` free. The gap
2020+ /// below where it is told keeps a disk that hovers at the edge (a read a
2021+ /// few KB either side) from showing and clearing its notice in turn.
2022+ pub const DISK_CLEAR_USED_PCT : u64 = 70 ;
2023+ pub const DISK_CLEAR_FREE_MIN : u64 = 6_000_000_000 ;
2024+ const _: ( ) = assert ! ( DISK_CLEAR_USED_PCT < DISK_TOLD_USED_PCT && DISK_CLEAR_FREE_MIN > DISK_TOLD_FREE_MAX , "it clears only past where it is told" ) ;
2025+
20142026/// Whether a disk of `total` bytes with `free` left is used past
20152027/// `DISK_TOLD_USED_PCT`, with at most `DISK_TOLD_FREE_MAX` free: its owner
20162028/// is told.
@@ -2019,6 +2031,25 @@ pub fn disk_filling(total: u64, free: u64) -> bool {
20192031 ( total - free) as u128 * 100 >= total as u128 * DISK_TOLD_USED_PCT as u128 && free <= DISK_TOLD_FREE_MAX
20202032}
20212033
2034+ /// Whether a disk told filling has clearly more room now: at most
2035+ /// `DISK_CLEAR_USED_PCT` used, or at least `DISK_CLEAR_FREE_MIN` free.
2036+ pub fn disk_clear ( total : u64 , free : u64 ) -> bool {
2037+ assert ! ( free <= total, "free fits in its disk" ) ;
2038+ ( total - free) as u128 * 100 <= total as u128 * DISK_CLEAR_USED_PCT as u128 || free >= DISK_CLEAR_FREE_MIN
2039+ }
2040+
2041+ /// The start whose disk to read once `event` was applied to `life`: the
2042+ /// one that just came up (its `Ready`), or an awake one whose save just
2043+ /// worked. Never before: a start is ready, and its deadline met, without
2044+ /// waiting on a read; and never a sleep's save, whose stop follows at once
2045+ /// (its next start reads it).
2046+ pub fn reads_disk_after ( event : & Event , life : & Lifecycle ) -> Option < u64 > {
2047+ match ( event, & life. phase ) {
2048+ ( Event :: Ready { generation : g } | Event :: Saved { generation : g, .. } , Phase :: Awake { generation, .. } ) if g == generation => Some ( * g) ,
2049+ _ => None ,
2050+ }
2051+ }
2052+
20222053/// What reads a computer's disk, run in its container (`disk_of_df` reads
20232054/// its answer): POSIX `df` in bytes, which GNU's and BusyBox's both print.
20242055pub const DISK_READ : & str = "df -P -B1 /" ;
@@ -2192,8 +2223,9 @@ pub fn support_url_ok(url: &str) -> bool {
21922223/// - `set_aside`: folders a start could not fit on its disk, so it started
21932224/// without them (`Aside::set_aside`), each kept until its owner gets it
21942225/// back or drops it;
2195- /// - `disk_filling`: its disk, as last read, is used past
2196- /// `DISK_TOLD_USED_PCT`, until a read finds it below that again.
2226+ /// - `disk_filling`: a read found its disk used past `DISK_TOLD_USED_PCT`
2227+ /// with at most `DISK_TOLD_FREE_MAX` free, and none since found clearly
2228+ /// more room (`disk_clear`).
21972229pub fn notices ( life : & Lifecycle , saves : & Saves , aside : & Aside , images : & Images , rules : & Rules ) -> Vec < ComputerNotice > {
21982230 let mut out = Vec :: with_capacity ( 6 ) ;
21992231 if let Phase :: Failed { why } = & life. phase {
@@ -2251,7 +2283,7 @@ pub fn notices(life: &Lifecycle, saves: &Saves, aside: &Aside, images: &Images,
22512283 if !aside. folders . is_empty ( ) {
22522284 out. push ( ComputerNotice :: SetAside { aside : aside. folders . iter ( ) . map ( AsideFolder :: view) . collect ( ) } ) ;
22532285 }
2254- if let Some ( d) = saves. disk . filter ( |d| disk_filling ( d . total , d . free ) ) {
2286+ if let Some ( d) = saves. disk . filter ( |_| saves . disk_told ) {
22552287 out. push ( ComputerNotice :: DiskFilling { total : d. total , free : d. free } ) ;
22562288 }
22572289 assert ! ( out. len( ) <= 6 , "one notice of each kind at most" ) ;
@@ -2891,35 +2923,80 @@ mod tests {
28912923
28922924 /// Goal (2026-11-03: a disk that filled left a computer that could not
28932925 /// start): its owner is told its disk is filling once a read finds it
2894- /// used past `DISK_TOLD_USED_PCT`, and no more once a read finds it
2895- /// below. Valid (the edge: exactly the share is told, a byte under is
2896- /// not), replay and order (a read of an earlier moment changes
2897- /// nothing), invalid (more free than its size is refused), saves
2898- /// stored before (no disk, nothing told). Method: the reads as the DO
2899- /// takes them, and what is told.
2926+ /// used past `DISK_TOLD_USED_PCT` with at most `DISK_TOLD_FREE_MAX`
2927+ /// free, and no more only once a read finds clearly more room
2928+ /// (`disk_clear`): a disk hovering at either edge, reads a few KB
2929+ /// apart, never shows and clears it in turn (Codex on #1015). Valid
2930+ /// (each edge, exactly), oscillation around both edges, replay and
2931+ /// order (a read of an earlier moment changes nothing), invalid (more
2932+ /// free than its size is refused), saves stored before (none told).
2933+ /// Method: the reads as the DO takes them, and what is told.
29002934 #[ test]
29012935 fn a_disk_filling_is_told_until_a_read_finds_room ( ) {
29022936 const GB : u64 = 1_000_000_000 ;
2937+ const KB : u64 = 8_192 ;
29032938 let told = |s : & Saves | notices ( & Lifecycle :: new ( ) , s, & Aside :: default ( ) , & Images :: default ( ) , & Rules :: default ( ) ) ;
29042939 assert ! ( disk_filling( 20 * GB , 4 * GB ) && !disk_filling( 20 * GB , 4 * GB + 1 ) , "80% used exactly is told, a byte under is not" ) ;
2905- assert ! ( disk_filling( 20 * GB , 0 ) && !disk_filling( 20 * GB , 20 * GB ) ) ;
29062940 assert ! ( !disk_filling( 2_000 * GB , 300 * GB ) , "a host's shared disk, 85% used with room to spare" ) ;
29072941 assert ! ( disk_filling( 2_000 * GB , 5 * GB ) && !disk_filling( 2_000 * GB , 5 * GB + 1 ) , "told once at most DISK_TOLD_FREE_MAX is free" ) ;
2942+ assert ! ( disk_clear( 20 * GB , 6 * GB ) && !disk_clear( 20 * GB , 6 * GB - 1 ) , "clear at 70% used, or 6 GB free" ) ;
2943+ assert ! ( disk_clear( 2_000 * GB , 6 * GB ) && !disk_clear( 2_000 * GB , 6 * GB - 1 ) ) ;
2944+ // a run of reads, each a moment later, and whether it is told after each
2945+ let run = |total : u64 , frees : & [ u64 ] | -> Vec < bool > {
2946+ let mut s = Saves :: default ( ) ;
2947+ frees. iter ( ) . enumerate ( ) . map ( |( i, free) | {
2948+ assert ! ( s. measured( ComputerDisk { total, free: * free, at: T + i as i64 } ) ) ;
2949+ matches ! ( told( & s) . as_slice( ) , [ ComputerNotice :: DiskFilling { total: t, free: f } ] if * t == total && * f == * free)
2950+ } ) . collect ( )
2951+ } ;
2952+ // around the told edge of a computer's own disk: shown, and it stays until 6 GB free
2953+ assert_eq ! ( run( 20 * GB , & [ 4 * GB + KB , 4 * GB , 4 * GB + KB , 4 * GB , 5 * GB , 6 * GB - 1 , 6 * GB , 6 * GB - KB , 4 * GB + KB , 4 * GB ] ) , [ false , true , true , true , true , true , false , false , false , true ] ) ;
2954+ // around the cleared edge: once clear, never told again until the told edge
2955+ assert_eq ! ( run( 20 * GB , & [ 4 * GB , 6 * GB , 6 * GB - KB , 6 * GB , 6 * GB - KB , 4 * GB + KB ] ) , [ true , false , false , false , false , false ] ) ;
2956+ // a host's shared disk, around 5 GB free
2957+ assert_eq ! ( run( 2_000 * GB , & [ 5 * GB + KB , 5 * GB , 5 * GB + KB , 6 * GB - KB , 6 * GB , 5 * GB + KB ] ) , [ false , true , true , true , false , false ] ) ;
2958+ // replay and order
29082959 let mut s = Saves :: default ( ) ;
29092960 assert ! ( told( & s) . is_empty( ) && s. disk( ) . is_none( ) , "never read: nothing told" ) ;
2910- assert ! ( s. measured( ComputerDisk { total: 20 * GB , free: 10 * GB , at: T } ) ) ;
2911- assert ! ( told( & s) . is_empty( ) , "half full" ) ;
29122961 assert ! ( s. measured( ComputerDisk { total: 20 * GB , free: 3 * GB , at: T + 10 } ) ) ;
2913- assert_eq ! ( told( & s) , vec![ ComputerNotice :: DiskFilling { total: 20 * GB , free: 3 * GB } ] ) ;
29142962 assert ! ( !s. measured( ComputerDisk { total: 20 * GB , free: 15 * GB , at: T + 5 } ) , "a late read of an earlier moment" ) ;
2915- assert_eq ! ( s . disk ( ) . map ( |d| d . free ) , Some ( 3 * GB ) ) ;
2963+ assert_eq ! ( told ( & s ) , vec! [ ComputerNotice :: DiskFilling { total : 20 * GB , free : 3 * GB } ] ) ;
29162964 assert ! ( s. measured( ComputerDisk { total: 20 * GB , free: 3 * GB , at: T + 10 } ) , "the same read again: the same" ) ;
2917- assert ! ( s. measured( ComputerDisk { total: 20 * GB , free: 6 * GB , at: T + 20 } ) ) ;
2918- assert ! ( told( & s) . is_empty( ) , "tidied: told no more" ) ;
2965+ assert_eq ! ( told( & s) . len( ) , 1 ) ;
29192966 assert ! ( std:: panic:: catch_unwind( || Saves :: default ( ) . measured( ComputerDisk { total: GB , free: 2 * GB , at: T } ) ) . is_err( ) , "more free than its size" ) ;
2967+ // saves stored before the disk was read, or before the latch: none told
29202968 let mut stored = serde_json:: to_value ( & s) . unwrap ( ) ;
29212969 stored. as_object_mut ( ) . unwrap ( ) . remove ( "disk" ) ;
2922- assert ! ( serde_json:: from_value:: <Saves >( stored) . unwrap( ) . disk( ) . is_none( ) ) ;
2970+ stored. as_object_mut ( ) . unwrap ( ) . remove ( "diskTold" ) ;
2971+ let old: Saves = serde_json:: from_value ( stored) . unwrap ( ) ;
2972+ assert ! ( old. disk( ) . is_none( ) && told( & old) . is_empty( ) ) ;
2973+ }
2974+
2975+ /// Goal (Codex on #1015: a read before `Ready` could push a start past
2976+ /// its deadline): a start's disk is read only once its `Ready` was
2977+ /// applied (the start awake, its deadline met), an awake save's once its
2978+ /// `Saved` was; never a late `Ready` of a start no longer under way, a
2979+ /// sleep's save (its stop follows), nor any other event. Method: the
2980+ /// lifecycle's steps, and what each says to read after.
2981+ #[ test]
2982+ fn a_disk_is_read_only_after_its_start_is_ready ( ) {
2983+ let mut l = Lifecycle :: new ( ) ;
2984+ l. apply ( Event :: Wake { why : Wake :: Owner } , T ) ;
2985+ assert_eq ! ( reads_disk_after( & Event :: Wake { why: Wake :: Owner } , & l) , None , "starting: nothing read" ) ;
2986+ // the deadline passes first: the late Ready is no start's, and nothing is read
2987+ let mut late = l. clone ( ) ;
2988+ late. apply ( Event :: Alarm , T + START_DEADLINE_MS ) ;
2989+ late. apply ( Event :: Ready { generation : 1 } , T + START_DEADLINE_MS + 1 ) ;
2990+ assert_eq ! ( reads_disk_after( & Event :: Ready { generation: 1 } , & late) , None ) ;
2991+ // ready within it: read after, the start awake and its alarm the awake one
2992+ let s = l. apply ( Event :: Ready { generation : 1 } , T + START_DEADLINE_MS - 1 ) ;
2993+ assert ! ( matches!( l. phase, Phase :: Awake { generation: 1 , .. } ) && s. alarm_ms. is_some_and( |a| a > T + START_DEADLINE_MS - 1 ) ) ;
2994+ assert_eq ! ( reads_disk_after( & Event :: Ready { generation: 1 } , & l) , Some ( 1 ) ) ;
2995+ // an awake save that worked: read after
2996+ assert_eq ! ( reads_disk_after( & Event :: Saved { generation: 1 , seq: 1 } , & l) , Some ( 1 ) ) ;
2997+ // a sleep's save: its stop follows, nothing read
2998+ l. apply ( Event :: Sleep , T + START_DEADLINE_MS + 10 ) ;
2999+ assert_eq ! ( reads_disk_after( & Event :: Saved { generation: 1 , seq: 1 } , & l) , None ) ;
29233000 }
29243001
29253002 /// Goal: a disk read from `df -P -B1 /` as GNU's (the Hermes image) and
@@ -4923,7 +5000,7 @@ mod tests {
49235000 reached[ 10 ] += 1 ;
49245001 }
49255002 ComputerNotice :: SetAside { aside } => assert ! ( !aside. is_empty( ) && aside. len( ) <= ASIDE_MAX , "set aside is told of what is (seed {seed0}): {n:?}" ) ,
4926- ComputerNotice :: DiskFilling { total, free } => assert ! ( disk_filling ( * total, * free) , "a disk is told filling only past its share (seed {seed0}): {n:?}" ) ,
5003+ ComputerNotice :: DiskFilling { total, free } => assert ! ( !disk_clear ( * total, * free) , "a disk told filling has no clear room (seed {seed0}): {n:?}" ) ,
49275004 }
49285005 }
49295006 // its owner puts an update off, now and then
0 commit comments