diegomrsantos commented on PR #4130: URL: https://github.com/apache/iggy/pull/4130#issuecomment-5796545995
Thanks @hubcio. Agreed on keeping the fix and regression tests here and discussing the broader design in #4145. I also created a small [Quint](https://quint.sh/docs/quint) model of purge and recovery to investigate the edge cases. Quint is a language for writing executable descriptions of a system’s behavior. We describe what survives a crash, which actions can happen, and which rules must always hold. Here, those rules include keeping purged messages and bookmarks from returning, while ensuring an old purge cutoff cannot hide fresh messages. Using TLC, a model checker supported by Quint, we can explore every reachable state of a small finite configuration. When a rule fails, it produces the sequence of events that caused the failure. That helps us examine combinations of crashes, retries, and replica recovery that are easy to overlook when writing individual tests. The model reproduces the cutoff mismatch we discussed and demonstrates problems with some apparent fixes. For example, clearing the cutoff on every restart can let a recovering replica replay purged messages and bookmarks from another replica that still retains the old journal. I think this could be a useful addition alongside the regression tests. It makes the recovery assumptions explicit, helps compare proposed fixes, and gives us concrete failure sequences to reproduce against the Rust implementation. Its conclusions depend on the model’s scope and assumptions, including how consensus selects a history, so it does not establish that the implementation is correct. Would you be open to keeping a small model alongside the tests as an executable explanation of the recovery rules? There is also a possible next step with [Quint Connect](https://github.com/quint-co/quint-connect). It can replay scenarios generated from a Quint model against real Rust code and compare the relevant state after each step. We would need a test driver that maps model actions to Iggy operations, controls the modeled failures, and translates Iggy’s state into the form the model expects. Those tests could run through `cargo test` in CI, helping catch cases where the implementation diverges from the recovery rules. That integration would still need to be built. -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: [email protected] For queries about this service, please contact Infrastructure at: [email protected]
