3636 GroupCompletenessPeek ,
3737 PeekChecker ,
3838 SubscribeChecker ,
39+ TernaryPartitionPeek ,
3940)
4041from materialize .invariants .framework import (
4142 CONVERGE_TIMEOUT ,
@@ -639,6 +640,131 @@ def check_once(self) -> None:
639640 self .validations += 1
640641
641642
643+ def ledger_predicate (rng : random .Random ) -> str :
644+ """A random total predicate over the ledger, for the partition oracle.
645+
646+ Total is the requirement: no division, no fallible cast, nothing that can
647+ raise, or the three branches of the partition fail differently instead of
648+ disagreeing. Everything here is a comparison, a NULL test, or a boolean
649+ combination of them.
650+
651+ The columns are chosen for the values that make filters and statistics
652+ pushdown awkward. `flt` carries NaN, both infinities, negative zero and a
653+ denormal, `day` is nullable, so predicates over it are the ones that put
654+ rows in the IS NULL branch at all, and `amount` is signed.
655+ """
656+ atoms = [
657+ f"amount > { rng .randint (- 100 , 100 )} " ,
658+ f"amount < { rng .randint (- 100 , 100 )} " ,
659+ f"amount = { rng .randint (- 100 , 100 )} " ,
660+ f"account >= { rng .randint (0 , 32 )} " ,
661+ f"seq % { rng .randint (2 , 9 )} = 0" ,
662+ "flt > 0" ,
663+ "flt < 0" ,
664+ "flt = 'NaN'::double precision" ,
665+ "flt = 'Infinity'::double precision" ,
666+ f"amount_dec > { rng .randint (- 100 , 100 )} " ,
667+ "tag LIKE 'w%'" ,
668+ f"tag LIKE '%s{ rng .randint (0 , 9 )} '" ,
669+ "day IS NULL" ,
670+ "day > DATE '2024-01-01'" ,
671+ f"day < DATE '20{ rng .randint (20 , 30 )} -06-01'" ,
672+ ]
673+ p = rng .choice (atoms )
674+ # Compound predicates, since a filter can be right on each half and wrong
675+ # on the combination, and NULL propagation through AND/OR is its own trap.
676+ if rng .random () < 0.4 :
677+ p = f"({ p } ) { rng .choice (['AND' , 'OR' ])} ({ rng .choice (atoms )} )"
678+ if rng .random () < 0.2 :
679+ p = f"NOT ({ p } )"
680+ return p
681+
682+
683+ # A DAG whose edges only ever point from a lower node to a higher one, so the
684+ # graph is acyclic no matter which inserts and deletes committed, and the
685+ # closure of whatever edges are currently visible is the thing to check. Small
686+ # enough that a dense closure stays bounded.
687+ GRAPH_NODES = 40
688+
689+ # Reachability recomputed from scratch, for comparison against the maintained
690+ # view. UNION rather than UNION ALL so the iteration converges.
691+ GRAPH_REACH_CTE = (
692+ "WITH MUTUALLY RECURSIVE reach (src int, dst int) AS ("
693+ " SELECT src, dst FROM edges"
694+ " UNION"
695+ " SELECT r.src, e.dst FROM reach r JOIN edges e ON r.dst = e.src"
696+ ")"
697+ )
698+ GRAPH_CLOSURE_SQL = f"{ GRAPH_REACH_CTE } SELECT src, dst FROM reach"
699+
700+ # Three properties of the closure of whatever edges are visible right now.
701+ # None of them depend on which operations succeeded, and each fails for a
702+ # different reason: a missing transitive pair means the iteration stopped
703+ # early, a missing edge means the base case was lost, and a self-loop means a
704+ # retraction left a cycle behind in a graph that cannot contain one.
705+ GRAPH_NOT_CLOSED_SQL = (
706+ "SELECT a.src, a.dst, b.dst FROM closure a"
707+ " JOIN closure b ON a.dst = b.src"
708+ " LEFT JOIN closure c ON c.src = a.src AND c.dst = b.dst"
709+ " WHERE c.src IS NULL LIMIT 5"
710+ )
711+ GRAPH_MISSING_EDGE_SQL = (
712+ "SELECT e.src, e.dst FROM edges e"
713+ " LEFT JOIN closure c ON c.src = e.src AND c.dst = e.dst"
714+ " WHERE c.src IS NULL LIMIT 5"
715+ )
716+ GRAPH_SELF_LOOP_SQL = "SELECT src, dst FROM closure WHERE src = dst LIMIT 5"
717+
718+ # The maintained view against the same question recomputed in one shot, at one
719+ # timestamp. This is the one that catches the incremental iteration diverging
720+ # from the batch answer, which is what retractions through a recursive
721+ # dataflow are most likely to get wrong.
722+ # The recursion is defined once and referenced from both sides: a WITH cannot
723+ # be an operand of a set operation, and this keeps it to one statement, so
724+ # both sides are answered at one timestamp.
725+ GRAPH_DIFFERENTIAL_SQL = (
726+ f"{ GRAPH_REACH_CTE } "
727+ " (SELECT src, dst FROM closure EXCEPT ALL SELECT src, dst FROM reach)"
728+ " UNION ALL"
729+ " (SELECT src, dst FROM reach EXCEPT ALL SELECT src, dst FROM closure)"
730+ )
731+
732+
733+ class GraphChurn (Action ):
734+ """Insert and delete edges of an acyclic graph.
735+
736+ Deletions are the point. An insert only ever grows the closure, which an
737+ iterative dataflow can get right by accumulating, while a delete has to
738+ retract every path that went through the removed edge, including paths
739+ discovered several iterations deep. Nothing else in this scenario asks the
740+ engine to iterate at all.
741+
742+ Edges always point from a lower node to a higher one, so the graph stays
743+ acyclic whatever subset of the operations applied, which is what lets the
744+ self-loop check be an invariant rather than a race.
745+ """
746+
747+ name = "graph-churn"
748+
749+ def __init__ (self , rng : random .Random , client : MzClient ) -> None :
750+ super ().__init__ (rng )
751+ self .client = client
752+
753+ def run (self ) -> Outcome | None :
754+ if self .rng .random () < 0.4 :
755+ # Delete by predicate rather than by a remembered edge: an
756+ # UNKNOWN insert may or may not exist, and this is correct either
757+ # way.
758+ src = self .rng .randrange (GRAPH_NODES - 1 )
759+ return self .client .write (f"DELETE FROM edges WHERE src = { src } " )
760+ src = self .rng .randrange (GRAPH_NODES - 1 )
761+ dst = self .rng .randrange (src + 1 , GRAPH_NODES )
762+ return self .client .write (f"INSERT INTO edges VALUES ({ src } , { dst } )" )
763+
764+ def close (self ) -> None :
765+ self .client .reset ()
766+
767+
642768class RollbackNoop (Action ):
643769 """A transaction that never commits must leave nothing behind.
644770
@@ -737,9 +863,22 @@ def __init__(self, rng: random.Random, client: MzClient, scenario) -> None:
737863
738864 def run (self ) -> Outcome | None :
739865 self .client .query (f"SET cluster = { self .rng .choice (['quickstart' , 'compute' ])} " )
740- return self .client .write_txn (
741- [("INSERT INTO cross_probe SELECT total FROM total" , None )]
742- )
866+ # A read and a write in one transaction, which is only expressible
867+ # this way: Materialize rejects both UPDATE and INSERT .. SELECT
868+ # inside a transaction block, so the read has to be its own statement
869+ # and the write has to carry the value the client saw.
870+ try :
871+ self .client .query ("BEGIN" )
872+ rows = self .client .query ("SELECT total FROM total" )
873+ self .client .query (f"INSERT INTO cross_probe VALUES ({ int (rows [0 ][0 ])} )" )
874+ self .client .query ("COMMIT" )
875+ except TransientError :
876+ self .client .reset ()
877+ raise
878+ except Exception :
879+ self .client .reset ()
880+ return Outcome .UNKNOWN
881+ return Outcome .COMMITTED
743882
744883 def close (self ) -> None :
745884 self .client .reset ()
@@ -1769,6 +1908,9 @@ def setup(self) -> None:
17691908 "CREATE TABLE counters (id int, n bigint)" ,
17701909 "CREATE TABLE rollback_probe (id bigint)" ,
17711910 "CREATE TABLE cross_probe (total bigint)" ,
1911+ "CREATE TABLE edges (src int, dst int)" ,
1912+ "CREATE MATERIALIZED VIEW closure IN CLUSTER compute AS"
1913+ f" { GRAPH_CLOSURE_SQL } " ,
17721914 f"INSERT INTO counters SELECT generate_series(0, { COUNTER_KEYS - 1 } ), 0" ,
17731915 * (
17741916 f"CREATE TABLE { table } (worker int, seq bigint, idx int)"
@@ -1829,12 +1971,13 @@ def make_worker(self, index: int, rng: random.Random) -> WorkerBundle:
18291971 ReadThenWrite (rng , index , client , self .counter_oplog ),
18301972 RollbackNoop (rng , index , self .ctx ),
18311973 CrossObjectTxn (rng , MzClient (self .ctx , f"cross-{ index } " ), self ),
1974+ GraphChurn (rng , MzClient (self .ctx , f"graph-{ index } " )),
18321975 ]
18331976 # The transfer actions carry the conservation and ledger-identity
18341977 # oracles, which are the strongest ones here, so they keep the bulk of
18351978 # the op budget. The rest only need to happen often enough to produce
18361979 # the states their checkers watch continuously.
1837- weights = [10 , 10 , 3 , 3 , 6 , 1 , 1 , 2 , 2 , 1 , 1 ]
1980+ weights = [10 , 10 , 3 , 3 , 6 , 1 , 1 , 2 , 2 , 1 , 1 , 3 ]
18381981 if index == 0 :
18391982 # Single-instance churns: concurrent swaps of the same schema
18401983 # pair or replacements of the same MV would only race each other
@@ -1847,7 +1990,7 @@ def make_worker(self, index: int, rng: random.Random) -> WorkerBundle:
18471990 return WorkerBundle (actions = actions , weights = weights )
18481991
18491992 def checkers (self ) -> list [Checker ]:
1850- rngs = [random .Random (self .ctx .rng .randrange (SEED_RANGE )) for _ in range (19 )]
1993+ rngs = [random .Random (self .ctx .rng .randrange (SEED_RANGE )) for _ in range (24 )]
18511994 return [
18521995 BankTotalPeek (rngs [0 ], self .ctx , self ),
18531996 LedgerDirectPeek (rngs [1 ], self .ctx , self ),
@@ -1870,6 +2013,31 @@ def checkers(self) -> list[Checker]:
18702013 ReplicaDivergence (rngs [14 ], self .ctx ),
18712014 CounterSumPeek (rngs [16 ], self .ctx , self .counter_oplog ),
18722015 RollbackProbePeek (rngs [17 ], self .ctx ),
2016+ GroupCompletenessPeek (
2017+ rngs [20 ], self .ctx , "closure-transitive" , GRAPH_NOT_CLOSED_SQL
2018+ ),
2019+ GroupCompletenessPeek (
2020+ rngs [21 ], self .ctx , "closure-has-edges" , GRAPH_MISSING_EDGE_SQL
2021+ ),
2022+ GroupCompletenessPeek (
2023+ rngs [22 ], self .ctx , "closure-acyclic" , GRAPH_SELF_LOOP_SQL
2024+ ),
2025+ GroupCompletenessPeek (
2026+ rngs [23 ],
2027+ self .ctx ,
2028+ "closure-differential" ,
2029+ GRAPH_DIFFERENTIAL_SQL ,
2030+ clusters = ["compute" ],
2031+ ),
2032+ TernaryPartitionPeek (
2033+ rngs [19 ],
2034+ self .ctx ,
2035+ "ledger-partition" ,
2036+ "ledger" ,
2037+ ledger_predicate ,
2038+ "amount" ,
2039+ history = self .recent_ts ,
2040+ ),
18732041 GroupCompletenessPeek (
18742042 rngs [18 ],
18752043 self .ctx ,
@@ -1935,6 +2103,15 @@ def final_check(self) -> None:
19352103 raise InvariantViolation (
19362104 f"a transaction reading the total MV recorded { wrong } , not { self .total } "
19372105 )
2106+ for name , sql in (
2107+ ("not transitively closed" , GRAPH_NOT_CLOSED_SQL ),
2108+ ("missing an edge" , GRAPH_MISSING_EDGE_SQL ),
2109+ ("has a self loop" , GRAPH_SELF_LOOP_SQL ),
2110+ ("disagrees with a recomputation" , GRAPH_DIFFERENTIAL_SQL ),
2111+ ):
2112+ bad = client .query (sql )
2113+ if bad :
2114+ raise InvariantViolation (f"closure { name } : { bad [:10 ]} " )
19382115 leaked = client .query ("SELECT id FROM rollback_probe LIMIT 20" )
19392116 if leaked :
19402117 raise InvariantViolation (
0 commit comments