Log non linearizable path when linearization check fails

cmd/dst/run.go

@@ -32,6 +32,7 @@
 		timeout           time.Duration
 		scenario          string
 		visualizationPath string
+		verbose           bool
 
 		reqsPerTick     = util.NewRangeIntFlag(1, 25)
 		ids             = util.NewRangeIntFlag(1, 25)
@@ -167,6 +168,7 @@
 				Ticks:              ticks,
 				Timeout:            timeout,
 				VisualizationPath:  visualizationPath,
+				Verbose:            verbose,
 				TimeElapsedPerTick: 1000, // ms
 				TimeoutTicks:       t,
 				ReqsPerTick:        func() int { return reqsPerTick.Resolve(r) },
@@ -206,6 +208,7 @@
 	cmd.Flags().DurationVar(&timeout, "timeout", 1*time.Hour, "timeout")
 	cmd.Flags().StringVar(&scenario, "scenario", "default", "can be one of: default, fault, lazy")
 	cmd.Flags().StringVar(&visualizationPath, "visualization-path", "dst.html", "porcupine visualization file path")
+	cmd.Flags().BoolVarP(&verbose, "verbose", "v", false, "log additional information when run is non linearizable")
 	cmd.Flags().Var(reqsPerTick, "reqs-per-tick", "number of requests per tick")
 	cmd.Flags().Var(ids, "ids", "promise id set size")
 	cmd.Flags().Var(idempotencyKeys, "idempotency-keys", "idempotency key set size")

test/dst/dst.go

@@ -29,6 +29,7 @@
 	Ticks              int64
 	Timeout            time.Duration
 	VisualizationPath  string
+	Verbose            bool
 	TimeElapsedPerTick int64
 	TimeoutTicks       int64
 	ReqsPerTick        func() int
@@ -49,6 +50,15 @@
 	Bc
 )
 
+type Partition int
+
+const (
+	Promise Partition = iota
+	Schedule
+	Lock
+	Task
+)
+
 type Req struct {
 	kind Kind
 	time int64
@@ -289,14 +299,64 @@
 	case porcupine.Ok:
 		slog.Info("DST is linearizable")
 	case porcupine.Illegal:
-		slog.Error("DST is non linearizable")
+		slog.Error("DST is non linearizable, run with -v flag for more information", "v", d.config.Verbose)
+		if d.config.Verbose {
+			d.logNonLinearizable(ops, history)
+		}
 	case porcupine.Unknown:
 		slog.Error("DST timed out before linearizability could be determined")
 	}
 
 	return result == porcupine.Ok
 }
 
+func (d *DST) logNonLinearizable(ops []porcupine.Operation, history porcupine.LinearizationInfo) {
+	// log the linearizations
+	linearizations := history.PartialLinearizationsOperations()
+	util.Assert(len(linearizations) == 3, "linearizations must be equal to the number of partitions")
+
+	// check each parition individually
+	// partitions are in order: promise, schedule, lock
+	for i, p := range []Partition{Promise, Schedule, Lock} {
+		util.Assert(len(linearizations[i]) > 0, "partition must have at least one linearization")
+
+		// take the first linearization
+		linearization := linearizations[i][0]
+
+		// determine the next operation that breaks linearizability
+		if next, ok := next(linearization, ops, p); ok {
+			// add the next operation to the linearization, so that we can log
+			// the non linearizable path
+			linearization = append(linearization, next)
+		} else {
+			// if no op is found, we can assume the partition is linearizable
+			continue
+		}
+
+		// re run and log operations
+		d.log(linearization)
+	}
+}
+
+func (d *DST) log(ops []porcupine.Operation) {
+	// create a new model
+	model := NewModel()
+
+	// re feed operations through model
+	for i, op := range ops {
+		req := op.Input.(*Req)
+		res := op.Output.(*Res)
+
+		var err error
+
+		// step through the model (again)
+		model, err = d.Step(model, req.time, res.time, req.req, res.res, res.err)
+		slog.Info("DST", "t", fmt.Sprintf("%d|%d", req.time, res.time), "id", req.req.Tags["id"], "req", req.req, "res", res.res, "err", err)
+
+		util.Assert(i != len(ops)-1 || err != nil, "the last operation must result in an error")
+	}
+}
+
 func (d *DST) Model() porcupine.Model {
 	return porcupine.Model{
 		Init: func() interface{} {
@@ -311,28 +371,16 @@
 			for _, op := range history {
 				req := op.Input.(*Req)
 
-				switch req.kind {
-				case Op:
-					switch req.req.Kind {
-					case t_api.ReadPromise, t_api.SearchPromises, t_api.CreatePromise, t_api.CompletePromise, t_api.CreateCallback:
-						p = append(p, op)
-					case t_api.ReadSchedule, t_api.SearchSchedules, t_api.CreateSchedule, t_api.DeleteSchedule:
-						s = append(s, op)
-					case t_api.AcquireLock, t_api.ReleaseLock, t_api.HeartbeatLocks:
-						l = append(l, op)
-					case t_api.ClaimTask, t_api.CompleteTask, t_api.HeartbeatTasks, t_api.CreatePromiseAndTask:
-						// TODO(avillega): Temporaly disable validations over tasks
-						// t = append(t, op)
-					default:
-						panic(fmt.Sprintf("unknown request kind: %s", req.req.Kind))
-					}
-				case Bc:
+				switch partition(req) {
+				case Promise:
+					p = append(p, op)
+				case Schedule:
+					s = append(s, op)
+				case Lock:
+					l = append(l, op)
 					// TODO(avillega): Temporaly disable validations over tasks
-					// if req.bc.Task != nil {
+					// case Task:
 					// 	t = append(t, op)
-					// }
-				default:
-					panic(fmt.Sprintf("unknown request kind: %d", req.kind))
 				}
 			}
 
@@ -343,7 +391,7 @@
 			req := input.(*Req)
 			res := output.(*Res)
 
-			util.Assert(req.kind == res.kind, "kinds must match ")
+			util.Assert(req.kind == res.kind, "kinds must match")
 
 			switch req.kind {
 			case Op:
@@ -422,7 +470,7 @@
 				}
 
 				return fmt.Sprintf(`
-					<table border="0" cellspacing="0" cellpadding="5">
+					<table border="0" cellspacing="0" cellpadding="5" style="background-color: white;">
 						<thead>
 							<tr>
 								<td><b>Promises</b></td>
@@ -476,7 +524,7 @@
 				}
 
 				return fmt.Sprintf(`
-					<table border="0" cellspacing="0" cellpadding="5">
+					<table border="0" cellspacing="0" cellpadding="5" style="background-color: white;">
 						<thead>
 							<tr>
 								<td><b>Schedules</b></td>
@@ -515,7 +563,7 @@
 				}
 
 				return fmt.Sprintf(`
-					<table border="0" cellspacing="0" cellpadding="5">
+					<table border="0" cellspacing="0" cellpadding="5" style="background-color: white;">
 						<thead>
 							<tr>
 								<td><b>Locks</b></td>
@@ -558,7 +606,7 @@
 				}
 
 				return fmt.Sprintf(`
-						<table border="0" cellspacing="0" cellpadding="5">
+						<table border="0" cellspacing="0" cellpadding="5" style="background-color: white;">
 							<thead>
 								<tr>
 									<td><b>Tasks</b></td>
@@ -644,3 +692,55 @@
 		cap(d.config.Backchannel),
 	)
 }
+
+// Helper functions
+
+func partition(req *Req) Partition {
+	switch req.kind {
+	case Op:
+		switch req.req.Kind {
+		case t_api.ReadPromise, t_api.SearchPromises, t_api.CreatePromise, t_api.CompletePromise, t_api.CreateCallback:
+			return Promise
+		case t_api.ReadSchedule, t_api.SearchSchedules, t_api.CreateSchedule, t_api.DeleteSchedule:
+			return Schedule
+		case t_api.AcquireLock, t_api.ReleaseLock, t_api.HeartbeatLocks:
+			return Lock
+		case t_api.ClaimTask, t_api.CompleteTask, t_api.HeartbeatTasks, t_api.CreatePromiseAndTask:
+			return Task
+		default:
+			panic(fmt.Sprintf("unknown request kind: %s", req.req.Kind))
+		}
+	case Bc:
+		return Task
+	default:
+		panic(fmt.Sprintf("unknown request kind: %d", req.kind))
+	}
+}
+
+func next(linearizable []porcupine.Operation, ops []porcupine.Operation, p Partition) (porcupine.Operation, bool) {
+	// convert to map for quick lookup
+	linearizableMap := map[porcupine.Operation]bool{}
+	for _, op := range linearizable {
+		linearizableMap[op] = true
+	}
+
+	for _, op := range ops {
+		req := op.Input.(*Req)
+
+		// if req is part of a different partition, skip
+		if partition(req) != p {
+			continue
+		}
+
+		// if req is part of the linearizable path, skip
+		if _, ok := linearizableMap[op]; ok {
+			continue
+		}
+
+		// ops are ordered by time, so the first op is not part of the
+		// linearizable path should break the model
+		return op, true
+	}
+
+	return porcupine.Operation{}, false
+}