aphyr
commented
3 years ago The lost updates in the Redis analysis manifest as divergence in the version order, which is reported as incompatible version orders in Elle--you can see examples in the case studies linked in the redis report. Elle doesn't have a precise definition of P4 (lost update) yet, so there's no anomaly called :lost-update in Elle's inferences. I'd love to do it, I just don't have a robust definition that maps to Adya's formalism yet. If you'd like to figure this out, please do--I'd like to add it. :)
Hello Jepsen Developers,
I have been testing Elle to capture the transaction anomalies with hand-written test-cases So far, G0 ~ G2 anomalies stated in the paper are all captured. But I'm a bit lost when I tried to implement the test-case for lost update which may not be described. I have found in Redis-Raft that Elle is used for capturing the lost updates for Redis. Would it be possible to have an example test case that shows Elle captures the lost-update?