From 4d2f9bde048983d0c4e93c3db93cb0814ce57ddd Mon Sep 17 00:00:00 2001 From: Anish Athalye Date: Sat, 27 Apr 2024 21:03:15 -0400 Subject: [PATCH] Add support for annotations in visualization --- README.md | 12 +++- checker.go | 5 -- visualization.go | 88 ++++++++++++++++++++++++++- visualization/index.css | 6 ++ visualization/index.js | 128 +++++++++++++++++++++++++++++++--------- visualization_test.go | 38 +++++++++++- 6 files changed, 238 insertions(+), 39 deletions(-) diff --git a/README.md b/README.md index aa68a71..e77871c 100644 --- a/README.md +++ b/README.md @@ -175,13 +175,13 @@ the case of a non-linearizable history). The result is an HTML page that draws an interactive visualization using JavaScript. The output looks like this:

- -Visualization demo + +Visualization demo

You can see the full interactive version -[here](https://anishathalye.github.io/porcupine/demo.html). +[here](https://anishathalye.github.io/porcupine/demo-annotations.html). The visualization is by partition: all partitions are essentially independent, so with the key-value store example above, operations related to each unique @@ -221,8 +221,14 @@ it's useful to fill out the `DescribeOperation` and `DescribeState` fields of the model. See [`visualization_test.go`](visualization_test.go) for an end-to-end example of how to visualize a history using Porcupine. +You can also add custom annotations to visualizations, as shown in the example +above. This can be helpful for attaching debugging information, e.g,. from +servers or the test framework. You can do this using the +[`AddAnnotations`][AddAnnotations] method. + [CheckOperationsVerbose]: https://pkg.go.dev/github.com/anishathalye/porcupine#CheckOperationsVerbose [CheckEventsVerbose]: https://pkg.go.dev/github.com/anishathalye/porcupine#CheckEventsVerbose +[AddAnnotations]: https://pkg.go.dev/github.com/anishathalye/porcupine#LinearizationInfo.AddAnnotations ## Notes diff --git a/checker.go b/checker.go index e9935c1..39c539f 100644 --- a/checker.go +++ b/checker.go @@ -21,11 +21,6 @@ type entry struct { clientId int } -type LinearizationInfo struct { - history [][]entry // for each partition, a list of entries - partialLinearizations [][][]int // for each partition, a set of histories (list of ids) -} - type byTime []entry func (a byTime) Len() int { diff --git a/visualization.go b/visualization.go index 87bb672..22a2770 100644 --- a/visualization.go +++ b/visualization.go @@ -9,6 +9,12 @@ import ( "sort" ) +type LinearizationInfo struct { + history [][]entry // for each partition, a list of entries + partialLinearizations [][][]int // for each partition, a set of histories (list of ids) + annotations []annotation +} + type historyElement struct { ClientId int Start int64 @@ -16,6 +22,18 @@ type historyElement struct { Description string } +type annotation struct { + ClientId int + Tag string + Start int64 + End int64 + Description string + Details string + Annotation bool // always true + TextColor string + BackgroundColor string +} + type linearizationStep struct { Index int StateDescription string @@ -29,11 +47,63 @@ type partitionVisualizationData struct { Largest map[int]int } -type visualizationData = []partitionVisualizationData +type visualizationData struct { + Partitions []partitionVisualizationData + Annotations []annotation +} + +// Annotations to add to histories. +// +// Either a ClientId or Tag must be supplied. The End is optional, for "point +// in time" annotations. If the end is left unspecified, the framework +// interprets it as Start. The text given in Description is shown in the main +// visualization, and the text given in Details (optional) is shown in the +// tooltip for the annotation. TextColor and BackgroundColor are both optional; +// if specified, they should be valid CSS colors, e.g., "#efaefc". +// +// To attach annotations to a visualization, use +// [LinearizationInfo.AddAnnotations]. +type Annotation struct { + ClientId int + Tag string + Start int64 + End int64 + Description string + Details string + TextColor string + BackgroundColor string +} + +// AddAnnotations adds extra annotations to a visualization. +// +// This can be used to add extra client operations or it can be used to add +// standalone annotations with arbitrary tags, e.g., associated with "servers" +// rather than clients, or even a "test framework". +// +// See documentation on [Annotation] for what kind of annotations you can add. +func (li *LinearizationInfo) AddAnnotations(annotations []Annotation) { + for _, elem := range annotations { + end := elem.End + if end < elem.Start { + end = elem.Start + } + li.annotations = append(li.annotations, annotation{ + ClientId: elem.ClientId, + Tag: elem.Tag, + Start: elem.Start, + End: end, + Description: elem.Description, + Details: elem.Details, + Annotation: true, + TextColor: elem.TextColor, + BackgroundColor: elem.BackgroundColor, + }) + } +} func computeVisualizationData(model Model, info LinearizationInfo) visualizationData { model = fillDefault(model) - data := make(visualizationData, len(info.history)) + partitions := make([]partitionVisualizationData, len(info.history)) for partition := 0; partition < len(info.history); partition++ { // history n := len(info.history[partition]) / 2 @@ -51,6 +121,9 @@ func computeVisualizationData(model Model, info LinearizationInfo) visualization history[elem.id].Description = model.DescribeOperation(callValue[elem.id], elem.value) returnValue[elem.id] = elem.value } + // historyElement.Annotation defaults to false, so we + // don't need to explicitly set it here; all of these + // are non-annotation elements } // partial linearizations largestIndex := make(map[int]int) @@ -78,12 +151,21 @@ func computeVisualizationData(model Model, info LinearizationInfo) visualization } linearizations[i] = linearization } - data[partition] = partitionVisualizationData{ + partitions[partition] = partitionVisualizationData{ History: history, PartialLinearizations: linearizations, Largest: largestIndex, } } + annotations := info.annotations + if annotations == nil { + annotations = make([]annotation, 0) + } + data := visualizationData{ + Partitions: partitions, + Annotations: annotations, + } + return data } diff --git a/visualization/index.css b/visualization/index.css index cf505e2..08d615c 100644 --- a/visualization/index.css +++ b/visualization/index.css @@ -42,6 +42,12 @@ text { fill: #42d1f5; } +.client-annotation-rect { + stroke: #888; + stroke-width: 1; + fill: #e0e0e0; +} + .link { fill: #206475; cursor: pointer; diff --git a/visualization/index.js b/visualization/index.js index d64ad1d..d58389a 100644 --- a/visualization/index.js +++ b/visualization/index.js @@ -56,19 +56,47 @@ function render(data) { const PADDING = 10 const BOX_HEIGHT = 30 const BOX_SPACE = 15 - const XOFF = 20 const EPSILON = 20 const LINE_BLEED = 5 const BOX_GAP = 20 const BOX_TEXT_PADDING = 10 const HISTORY_RECT_RADIUS = 4 + const annotations = data['Annotations'] + const coreHistory = data['Partitions'] + // for simplicity, make annotations look like more history + const allData = [...coreHistory, { History: annotations }] + let maxClient = -1 - data.forEach((partition) => { + allData.forEach((partition) => { partition['History'].forEach((el) => { maxClient = Math.max(maxClient, el['ClientId']) }) }) + // "real" clients, not including tags + const realClients = maxClient + 1 + // we treat each unique annotation tag as another "client" + const tags = new Set() + annotations.forEach((annot) => { + const tag = annot['Tag'] + if (tag.length !== 0) { + tags.add(tag) + } + }) + // add synthetic client numbers + const tag2ClientId = {} + const sortedTags = Array.from(tags).sort() + sortedTags.forEach((tag) => { + maxClient = maxClient + 1 + tag2ClientId[tag] = maxClient + }) + annotations.forEach((annot) => { + const tag = annot['Tag'] + if (tag.length !== 0) { + annot['ClientId'] = tag2ClientId[tag] + } + }) + // total number of clients now includes these synthetic clients const nClient = maxClient + 1 // Prepare some useful data to be used later: @@ -80,7 +108,7 @@ function render(data) { const startTimestamps = new Set() let gid = 0 const byGid = {} - data.forEach((partition) => { + allData.forEach((partition) => { partition['History'].forEach((el) => { allTimestamps.add(el['Start']) startTimestamps.add(el['Start']) @@ -103,7 +131,7 @@ function render(data) { for (let i = 0; i < sortedTimestamps.length - 1; i++) { nextTs[sortedTimestamps[i]] = sortedTimestamps[i + 1] } - data.forEach((partition) => { + allData.forEach((partition) => { partition['History'].forEach((el) => { let end = el['End'] el['OriginalEnd'] = end // for display purposes @@ -155,7 +183,7 @@ function render(data) { const xPos = {} // Compute some information about history elements, sorted by end time; // the most important information here is box width. - const byEnd = data + const byEnd = allData .flatMap((partition) => partition['History'].map((el) => { // compute width of the text inside the history element by actually @@ -186,7 +214,7 @@ function render(data) { const eventIllegalLast = newArray(gid, () => []) // event -> [index] const allLinearizations = [] let lgid = 0 - data.forEach((partition) => { + coreHistory.forEach((partition) => { partition['PartialLinearizations'].forEach((lin) => { const globalized = [] // linearization with global indexes instead of partition-local ones const included = new Set() // for figuring out illegal next LPs @@ -277,13 +305,33 @@ function render(data) { xPos[ts] = pos } + // get maximum tag width + let maxTagWidth = 0 + for (let i = 0; i < nClient; i++) { + const tag = i < realClients ? i.toString() : sortedTags[i - realClients] + const scratch = document.getElementById('calc') + scratch.innerHTML = '' + const svg = svgadd(scratch, 'svg') + const text = svgadd(svg, 'text', { + 'text-anchor': 'end', + }) + text.textContent = tag + const bbox = text.getBBox() + const width = bbox.width + 2 * BOX_TEXT_PADDING + if (width > maxTagWidth) { + maxTagWidth = width + } + } + + const t0x = PADDING + maxTagWidth // X-pos of line at t=0 + // Solved, now draw UI. let selected = false let selectedIndex = [-1, -1] const height = 2 * PADDING + BOX_HEIGHT * nClient + BOX_SPACE * (nClient - 1) - const width = 2 * PADDING + XOFF + xPos[sortedTimestamps[sortedTimestamps.length - 1]] + const width = 2 * PADDING + maxTagWidth + xPos[sortedTimestamps[sortedTimestamps.length - 1]] const svg = svgadd(document.getElementById('canvas'), 'svg', { width: width, height: height, @@ -301,25 +349,37 @@ function render(data) { bgRect.onclick = handleBgClick for (let i = 0; i < nClient; i++) { const text = svgadd(bg, 'text', { - x: XOFF / 2, + x: PADDING + maxTagWidth - BOX_TEXT_PADDING, y: PADDING + BOX_HEIGHT / 2 + i * (BOX_HEIGHT + BOX_SPACE), - 'text-anchor': 'middle', + 'text-anchor': 'end', }) - text.textContent = i + text.textContent = i < realClients ? i : sortedTags[i - realClients] } + // vertical line at t=0 svgadd(bg, 'line', { - x1: PADDING + XOFF, + x1: t0x, y1: PADDING, - x2: PADDING + XOFF, + x2: t0x, y2: height - PADDING, class: 'divider', }) + // horizontal line dividing clients from annotation tags, but only if there are tags + if (tags.size > 0) { + const annotationLineY = PADDING + realClients * (BOX_HEIGHT + BOX_SPACE) - BOX_SPACE / 2 + svgadd(bg, 'line', { + x1: PADDING, + y1: annotationLineY, + x2: t0x, + y2: annotationLineY, + class: 'divider', + }) + } // draw history const historyLayers = [] const historyRects = [] const targetRects = svgnew('g') - data.forEach((partition, partitionIndex) => { + allData.forEach((partition, partitionIndex) => { const l = svgadd(svg, 'g') historyLayers.push(l) const rects = [] @@ -327,8 +387,9 @@ function render(data) { const g = svgadd(l, 'g') const rx = xPos[el['Start']] const width = xPos[el['End']] - rx - const x = rx + XOFF + PADDING + const x = rx + t0x const y = PADDING + el['ClientId'] * (BOX_HEIGHT + BOX_SPACE) + const rectClass = el['Annotation'] ? 'client-annotation-rect' : 'history-rect' rects.push( svgadd(g, 'rect', { height: BOX_HEIGHT, @@ -337,7 +398,11 @@ function render(data) { y: y, rx: HISTORY_RECT_RADIUS, ry: HISTORY_RECT_RADIUS, - class: 'history-rect', + class: rectClass, + style: + el['Annotation'] && el['BackgroundColor'].length !== 0 + ? `fill: ${el['BackgroundColor']};` + : '', }) ) const text = svgadd(g, 'text', { @@ -345,6 +410,7 @@ function render(data) { y: y + BOX_HEIGHT / 2, 'text-anchor': 'middle', class: 'history-text', + style: el['Annotation'] && el['TextColor'].length !== 0 ? `fill: ${el['TextColor']};` : '', }) text.textContent = el['Description'] // we don't add mouseTarget to g, but to targetRects, because we @@ -369,18 +435,18 @@ function render(data) { }) // draw partial linearizations - const illegalLast = data.map((partition) => { + const illegalLast = coreHistory.map((partition) => { return partition['PartialLinearizations'].map(() => new Set()) }) - const largestIllegal = data.map(() => { + const largestIllegal = coreHistory.map(() => { return {} }) - const largestIllegalLength = data.map(() => { + const largestIllegalLength = coreHistory.map(() => { return {} }) const partialLayers = [] const errorPoints = [] - data.forEach((partition, partitionIndex) => { + coreHistory.forEach((partition, partitionIndex) => { const l = [] partialLayers.push(l) partition['PartialLinearizations'].forEach((lin, linIndex) => { @@ -392,7 +458,7 @@ function render(data) { const included = new Set() lin.forEach((id) => { const el = partition['History'][id['Index']] - const hereX = PADDING + XOFF + xPos[el['Start']] + const hereX = t0x + xPos[el['Start']] const x = prevX !== null ? Math.max(hereX, prevX + EPSILON) : hereX const y = PADDING + el['ClientId'] * (BOX_HEIGHT + BOX_SPACE) - LINE_BLEED // line from previous @@ -430,7 +496,7 @@ function render(data) { }) partition['History'].forEach((el, index) => { if (!included.has(index) && el['Start'] < minEnd) { - const hereX = PADDING + XOFF + xPos[el['Start']] + const hereX = t0x + xPos[el['Start']] const x = prevX !== null ? Math.max(hereX, prevX + EPSILON) : hereX const y = PADDING + el['ClientId'] * (BOX_HEIGHT + BOX_SPACE) - LINE_BLEED // line from previous @@ -487,8 +553,12 @@ function render(data) { function linearizationIndex(partition, index) { // show this linearization - if (Object.prototype.hasOwnProperty.call(data[partition]['Largest'], index)) { - return data[partition]['Largest'][index] + if (partition >= coreHistory.length) { + // annotation + return null + } + if (Object.prototype.hasOwnProperty.call(coreHistory[partition]['Largest'], index)) { + return coreHistory[partition]['Largest'][index] } else if (Object.prototype.hasOwnProperty.call(largestIllegal[partition], index)) { return largestIllegal[partition][index] } @@ -533,7 +603,11 @@ function render(data) { // if selected, show info relevant to the selected linearization maxIndex = linearizationIndex(sPartition, sIndex) } - if (selected && sPartition !== partition) { + if (partition >= coreHistory.length) { + // annotation + const details = annotations[index]['Details'] + tooltip.innerHTML = details.length === 0 ? '⟨no details⟩' : details + } else if (selected && sPartition !== partition) { tooltip.innerHTML = 'Not part of selected partition.' } else if (maxIndex === null) { if (!selected) { @@ -542,7 +616,7 @@ function render(data) { tooltip.innerHTML = 'Selected element is not part of any partial linearization.' } } else { - const lin = data[partition]['PartialLinearizations'][maxIndex] + const lin = coreHistory[partition]['PartialLinearizations'][maxIndex] let prev = null, curr = null let found = false @@ -554,8 +628,8 @@ function render(data) { break } } - let call = data[partition]['History'][index]['Start'] - let ret = data[partition]['History'][index]['OriginalEnd'] + let call = allData[partition]['History'][index]['Start'] + let ret = allData[partition]['History'][index]['OriginalEnd'] let msg = '' if (found) { // part of linearization diff --git a/visualization_test.go b/visualization_test.go index 8777240..44ce337 100644 --- a/visualization_test.go +++ b/visualization_test.go @@ -60,7 +60,7 @@ func TestVisualizationMultipleLengths(t *testing.T) { }, Largest: map[int]int{0: 0, 1: 0}, }} - if !reflect.DeepEqual(expected, data) { + if !reflect.DeepEqual(expected, data.Partitions) { t.Fatalf("expected data to be \n%v\n, was \n%v", expected, data) } visualizeTempFile(t, kvModel, info) @@ -127,3 +127,39 @@ func TestVisualizationLarge(t *testing.T) { visualizeTempFile(t, etcdModel, info) } + +func TestVisualizationAnnotations(t *testing.T) { + // base set of operations same as TestVisualizationMultipleLengths + ops := []Operation{ + {0, kvInput{op: 0, key: "x"}, 0, kvOutput{"w"}, 100}, + {1, kvInput{op: 1, key: "x", value: "y"}, 5, kvOutput{}, 10}, + {2, kvInput{op: 1, key: "x", value: "z"}, 0, kvOutput{}, 10}, + {1, kvInput{op: 0, key: "x"}, 20, kvOutput{"y"}, 30}, + {1, kvInput{op: 1, key: "x", value: "w"}, 35, kvOutput{}, 45}, + {5, kvInput{op: 0, key: "x"}, 25, kvOutput{"z"}, 35}, + {3, kvInput{op: 0, key: "x"}, 30, kvOutput{"y"}, 40}, + {4, kvInput{op: 0, key: "y"}, 50, kvOutput{"a"}, 90}, + {2, kvInput{op: 1, key: "y", value: "a"}, 55, kvOutput{}, 85}, + } + res, info := CheckOperationsVerbose(kvModel, ops, 0) + annotations := []Annotation{ + // let's say that there was a "failed get" by client 4 early on + {ClientId: 4, Start: 10, End: 31, Description: "get('y') timeout", BackgroundColor: "#ff9191"}, + // and a failed get by client 5 later + {ClientId: 5, Start: 80, Description: "get('x') timeout", BackgroundColor: "#ff9191"}, + // and some tagged annotations + {Tag: "Server 1", Start: 30, Description: "leader", Details: "became leader in term 3 with 2 votes"}, + {Tag: "Server 3", Start: 10, Description: "duplicate", Details: "saw duplicate operation put('x', 'y')"}, + {Tag: "Server 2", Start: 80, Description: "restart"}, + {Tag: "Server 3", Start: 0, Description: "leader", Details: "became leader in term 1 with 3 votes"}, + // and some "test framework" annotations + {Tag: "Test Framework", Start: 20, End: 35, Description: "partition [3] [1 2]", BackgroundColor: "#efaefc"}, + {Tag: "Test Framework", Start: 40, End: 100, Description: "partition [2] [1 3]", BackgroundColor: "#efaefc"}, + } + info.AddAnnotations(annotations) + if res != Illegal { + t.Fatalf("expected output %v, got output %v", Illegal, res) + } + // we don't check much else here, this has to be visually inspected + visualizeTempFile(t, kvModel, info) +}