Skip to content

Commit

Permalink
Log non linearizable path when linearization check fails (#498)
Browse files Browse the repository at this point in the history
  • Loading branch information
@dfarr
dfarr authored Dec 18, 2024
1 parent 3009bbb commit 0cecd95
Show file tree
Hide file tree
Showing 2 changed files with 129 additions and 26 deletions.
3 changes: 3 additions & 0 deletions cmd/dst/run.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ func RunDSTCmd() *cobra.Command {
timeout time.Duration
scenario string
visualizationPath string
verbose bool

reqsPerTick = util.NewRangeIntFlag(1, 25)
ids = util.NewRangeIntFlag(1, 25)
Expand Down Expand Up @@ -167,6 +168,7 @@ func RunDSTCmd() *cobra.Command {
Ticks: ticks,
Timeout: timeout,
VisualizationPath: visualizationPath,
Verbose: verbose,
TimeElapsedPerTick: 1000, // ms
TimeoutTicks: t,
ReqsPerTick: func() int { return reqsPerTick.Resolve(r) },
Expand Down Expand Up @@ -206,6 +208,7 @@ func RunDSTCmd() *cobra.Command {
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")
Expand Down
152 changes: 126 additions & 26 deletions test/dst/dst.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ type Config struct {
Ticks int64
Timeout time.Duration
VisualizationPath string
Verbose bool
TimeElapsedPerTick int64
TimeoutTicks int64
ReqsPerTick func() int
Expand All @@ -49,6 +50,15 @@ const (
Bc
)

type Partition int

const (
Promise Partition = iota
Schedule
Lock
Task
)

type Req struct {
kind Kind
time int64
Expand Down Expand Up @@ -289,14 +299,64 @@ func (d *DST) Run(r *rand.Rand, api api.API, aio aio.AIO, system *system.System)
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{} {
Expand All @@ -311,28 +371,16 @@ func (d *DST) Model() porcupine.Model {
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))
}
}

Expand All @@ -343,7 +391,7 @@ func (d *DST) Model() porcupine.Model {
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:
Expand Down Expand Up @@ -422,7 +470,7 @@ func (d *DST) Model() porcupine.Model {
}

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>
Expand Down Expand Up @@ -476,7 +524,7 @@ func (d *DST) Model() porcupine.Model {
}

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>
Expand Down Expand Up @@ -515,7 +563,7 @@ func (d *DST) Model() porcupine.Model {
}

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>
Expand Down Expand Up @@ -558,7 +606,7 @@ func (d *DST) Model() porcupine.Model {
}

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>
Expand Down Expand Up @@ -644,3 +692,55 @@ func (d *DST) String() string {
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
}

0 comments on commit 0cecd95

Please sign in to comment.