From 6863e2e4eccf77b5d318d9eac1386a5fbcfc586f Mon Sep 17 00:00:00 2001 From: Samuel Date: Mon, 12 Oct 2026 22:33:35 -0400 Subject: [PATCH 1/3] feat: add trace state snapshots and automated Playwright visualizer CI Enrich TraceRecord with per-configuration StateSnapshot records (shared fields and per-thread locals) captured during replay and emitted in --json reports. Update visualizer.js and visualizer.css to render live state strip tables with diff highlighting between consecutive steps independently of external program JSON. Add an automated headless Playwright test suite in docs/visualizer-e2e.mjs integrated into .github/workflows/build.yml to verify verdict rendering, timeline selection, keyboard accessibility, and state strip values in CI. Co-authored-by: Codex --- .github/workflows/build.yml | 10 +- .gitignore | 1 + docs/package-lock.json | 42 +++ docs/package.json | 11 + docs/visualizer-e2e.mjs | 239 +++++++++++++++ docs/visualizer.css | 1 + docs/visualizer.js | 278 ++++++++++++++---- examples/traces/lost-update.json | 9 +- .../samhb/interleave/InterleaveRunner.java | 46 ++- .../dev/samhb/interleave/TraceRecord.java | 43 ++- .../samhb/interleave/core/CounterState.java | 8 + .../samhb/interleave/core/DeadlockState.java | 8 + .../samhb/interleave/core/StateSnapshot.java | 68 +++++ .../core/StateSnapshotExtractor.java | 127 ++++++++ .../interleave/report/BenchmarkHarness.java | 26 +- .../interleave/report/BenchmarkResult.java | 40 +++ .../samhb/interleave/report/ReportWriter.java | 17 +- .../interleave/search/TraceReplayer.java | 57 ++++ .../dev/samhb/interleave/TraceRecordTest.java | 76 +++++ .../core/StateSnapshotExtractorTest.java | 153 ++++++++++ .../interleave/search/TraceReplayerTest.java | 41 +++ 21 files changed, 1210 insertions(+), 91 deletions(-) create mode 100644 docs/package-lock.json create mode 100644 docs/package.json create mode 100644 docs/visualizer-e2e.mjs create mode 100644 src/main/java/dev/samhb/interleave/core/StateSnapshot.java create mode 100644 src/main/java/dev/samhb/interleave/core/StateSnapshotExtractor.java create mode 100644 src/test/java/dev/samhb/interleave/TraceRecordTest.java create mode 100644 src/test/java/dev/samhb/interleave/core/StateSnapshotExtractorTest.java diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index a887c9a..accca75 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -33,8 +33,14 @@ jobs: node-version: "24" package-manager-cache: false - - name: Check visualizer verdict compatibility - run: node docs/visualizer-normalize-check.mjs + - name: Install dependencies + run: npm ci --prefix docs + + - name: Install Playwright browsers + run: npx --prefix docs playwright install --with-deps chromium + + - name: Run visualizer test suite + run: npm test --prefix docs build: name: Build diff --git a/.gitignore b/.gitignore index bc65faa..02d3abe 100644 --- a/.gitignore +++ b/.gitignore @@ -13,3 +13,4 @@ out/ gradle-app.setting !gradle-wrapper.jar !gradle-wrapper.properties +node_modules/ diff --git a/docs/package-lock.json b/docs/package-lock.json new file mode 100644 index 0000000..da4eb19 --- /dev/null +++ b/docs/package-lock.json @@ -0,0 +1,42 @@ +{ + "name": "interleave-visualizer", + "lockfileVersion": 3, + "requires": true, + "packages": { + "": { + "name": "interleave-visualizer", + "devDependencies": { + "playwright": "^1.50.0" + } + }, + "node_modules/playwright": { + "version": "1.64.0", + "resolved": "https://registry.npmjs.org/playwright/-/playwright-1.64.0.tgz", + "integrity": "sha512-kVzTnYFYEyQ9RGzBjNCd2+yEqWmVbxl3AHPynv3qQ6JTjv4a+kwRcnqQwIpuP3NnrnIrE/Q6wWAIAvMfIE2/Yg==", + "dev": true, + "license": "Apache-2.0", + "dependencies": { + "playwright-core": "1.64.0" + }, + "bin": { + "playwright": "cli.js" + }, + "engines": { + "node": ">=20" + } + }, + "node_modules/playwright-core": { + "version": "1.64.0", + "resolved": "https://registry.npmjs.org/playwright-core/-/playwright-core-1.64.0.tgz", + "integrity": "sha512-T9r+MZkTECl2+oUcZ26YgZzTrYidTsIhYYkJix+6iDOymOb1FB2RLLSOxRGnZGv5DStt+aduIVbt+E8WygXYpg==", + "dev": true, + "license": "Apache-2.0", + "bin": { + "playwright-core": "cli.js" + }, + "engines": { + "node": ">=20" + } + } + } +} diff --git a/docs/package.json b/docs/package.json new file mode 100644 index 0000000..481e3e7 --- /dev/null +++ b/docs/package.json @@ -0,0 +1,11 @@ +{ + "name": "interleave-visualizer", + "private": true, + "type": "module", + "scripts": { + "test": "node visualizer-normalize-check.mjs && node visualizer-e2e.mjs" + }, + "devDependencies": { + "playwright": "^1.50.0" + } +} diff --git a/docs/visualizer-e2e.mjs b/docs/visualizer-e2e.mjs new file mode 100644 index 0000000..4cb587f --- /dev/null +++ b/docs/visualizer-e2e.mjs @@ -0,0 +1,239 @@ +// Automated end-to-end browser tests for docs/visualizer.html using Playwright. +// Tests DOM rendering, user interactions, keyboard navigation, state snapshot display, +// and console message integrity. +// +// Run: node docs/visualizer-e2e.mjs + +import { createServer } from 'node:http'; +import { readFileSync, existsSync } from 'node:fs'; +import { join, extname, dirname } from 'node:path'; +import { fileURLToPath } from 'node:url'; +import { chromium } from 'playwright'; + +const __filename = fileURLToPath(import.meta.url); +const __dirname = dirname(__filename); +const projectRoot = join(__dirname, '..'); + +const MIME_TYPES = { + '.html': 'text/html; charset=utf-8', + '.js': 'application/javascript; charset=utf-8', + '.css': 'text/css; charset=utf-8', + '.json': 'application/json; charset=utf-8', + '.ico': 'image/x-icon' +}; + +// Start a lightweight static server for test files +function createStaticServer() { + return createServer((req, res) => { + try { + const urlPath = new URL(req.url, 'http://localhost').pathname; + let filePath; + + if (urlPath === '/' || urlPath === '/visualizer.html') { + filePath = join(__dirname, 'visualizer.html'); + } else if (urlPath.startsWith('/docs/')) { + filePath = join(__dirname, urlPath.slice(6)); + } else if (urlPath.startsWith('/examples/')) { + filePath = join(projectRoot, urlPath.slice(1)); + } else if (urlPath.startsWith('/src/')) { + filePath = join(projectRoot, urlPath.slice(1)); + } else { + filePath = join(__dirname, urlPath.slice(1)); + } + + if (existsSync(filePath)) { + const ext = extname(filePath); + const mime = MIME_TYPES[ext] || 'application/octet-stream'; + const data = readFileSync(filePath); + res.writeHead(200, { 'Content-Type': mime, 'Access-Control-Allow-Origin': '*' }); + res.end(data); + } else { + res.writeHead(404, { 'Content-Type': 'text/plain' }); + res.end(`File not found: ${urlPath}`); + } + } catch (err) { + res.writeHead(500, { 'Content-Type': 'text/plain' }); + res.end(`Internal server error: ${err.message}`); + } + }); +} + +async function runTests() { + const server = createStaticServer(); + await new Promise((resolve) => server.listen(0, '127.0.0.1', resolve)); + const port = server.address().port; + const baseUrl = `http://127.0.0.1:${port}/visualizer.html`; + console.log(`Test server running at ${baseUrl}`); + + let passed = 0; + let failed = 0; + + const assert = (condition, msg) => { + if (condition) { + console.log(` PASS: ${msg}`); + passed++; + } else { + console.error(` FAIL: ${msg}`); + failed++; + } + }; + + const browser = await chromium.launch({ headless: true }); + const context = await browser.newContext(); + const page = await context.newPage(); + + const consoleErrors = []; + page.on('console', (msg) => { + if (msg.type() === 'error') { + consoleErrors.push(msg.text()); + } + }); + page.on('pageerror', (err) => { + consoleErrors.push(err.message); + }); + + try { + // ------------------------------------------------------------- + // Test 1: Page Load and Initial Clean State + // ------------------------------------------------------------- + console.log('\nTest 1: Initial page state'); + await page.goto(baseUrl); + const title = await page.title(); + assert(title.includes('interleave'), 'Page title contains "interleave"'); + + const badgeText = await page.locator('#verdictBadge').textContent(); + assert(badgeText === '—', 'Verdict badge initialized with "—"'); + + // ------------------------------------------------------------- + // Test 2: Load lost-update.json via paste & verify snapshot strip + // ------------------------------------------------------------- + console.log('\nTest 2: Load lost-update.json with snapshot states'); + const lostUpdateJson = readFileSync(join(projectRoot, 'examples/traces/lost-update.json'), 'utf8'); + await page.locator('#paste').fill(lostUpdateJson); + await page.locator('#loadPaste').click(); + + const verdictLostUpdate = await page.locator('#verdictBadge').textContent(); + assert(verdictLostUpdate === 'VIOLATION', 'lost-update renders VIOLATION verdict'); + + const stepCount = await page.locator('#stepCount').textContent(); + assert(stepCount === '4', 'Step count is 4'); + + const timelineRows = page.locator('#timeline tbody tr'); + const rowCount = await timelineRows.count(); + assert(rowCount === 5, 'Timeline renders 5 configurations (0 to 4)'); + + // Row 4 should be active by default (selectedIdx = trace length) + const activeRow4 = timelineRows.nth(4); + assert(await activeRow4.evaluate((el) => el.classList.contains('active-row')), 'Final row 4 is active by default'); + assert(await activeRow4.getAttribute('aria-pressed') === 'true', 'Row 4 has aria-pressed="true"'); + + // State strip for config 4 should show counter = 1 + const config4Label = await page.locator('#selectedIdxLabel').textContent(); + assert(config4Label.includes('config 4'), 'State strip header shows config 4'); + + const stateCells = await page.locator('#stateStrip table tbody tr').allTextContents(); + const counterRow4 = stateCells.find((row) => row.includes('counter')); + assert(counterRow4 != null && counterRow4.includes('1'), 'State strip at config 4 displays counter = 1'); + + // ------------------------------------------------------------- + // Test 3: Interactive Row Click & State Diff Highlighting + // ------------------------------------------------------------- + console.log('\nTest 3: Interactive timeline selection and diff highlight'); + // Click config 3 (where counter became 1) + await timelineRows.nth(3).click(); + assert(await timelineRows.nth(3).evaluate((el) => el.classList.contains('active-row')), 'Row 3 becomes active on click'); + assert(await timelineRows.nth(4).evaluate((el) => !el.classList.contains('active-row')), 'Row 4 is no longer active'); + + const config3Label = await page.locator('#selectedIdxLabel').textContent(); + assert(config3Label.includes('config 3'), 'State strip header updates to config 3'); + + // In config 3, counter changed from 0 to 1, so .val-changed should be present + const changedCellCount3 = await page.locator('#stateStrip .val-changed').count(); + assert(changedCellCount3 > 0, 'State strip contains highlighted .val-changed cells on value change'); + + // Click config 0 (initial state: counter = 0) + await timelineRows.nth(0).click(); + assert(await timelineRows.nth(0).evaluate((el) => el.classList.contains('active-row')), 'Row 0 becomes active on click'); + const stateCells0 = await page.locator('#stateStrip table tbody tr').allTextContents(); + const counterRow0 = stateCells0.find((row) => row.includes('counter')); + assert(counterRow0 != null && counterRow0.includes('0'), 'State strip at config 0 displays counter = 0'); + + // ------------------------------------------------------------- + // Test 4: Keyboard Navigation (Enter and Space) + // ------------------------------------------------------------- + console.log('\nTest 4: Keyboard navigation'); + const row2 = timelineRows.nth(2); + await row2.focus(); + await page.keyboard.press('Enter'); + assert(await row2.evaluate((el) => el.classList.contains('active-row')), 'Pressing Enter activates row 2'); + const config2Label = await page.locator('#selectedIdxLabel').textContent(); + assert(config2Label.includes('config 2'), 'State strip updates to config 2 via Enter'); + + const row1 = timelineRows.nth(1); + await row1.focus(); + await page.keyboard.press('Space'); + assert(await row1.evaluate((el) => el.classList.contains('active-row')), 'Pressing Space activates row 1'); + const config1Label = await page.locator('#selectedIdxLabel').textContent(); + assert(config1Label.includes('config 1'), 'State strip updates to config 1 via Space'); + + // ------------------------------------------------------------- + // Test 5: Load peterson.json (PASS verdict) + // ------------------------------------------------------------- + console.log('\nTest 5: Load peterson.json fixture'); + const petersonJson = readFileSync(join(projectRoot, 'examples/traces/peterson.json'), 'utf8'); + await page.locator('#clearBtn').click(); + await page.locator('#paste').fill(petersonJson); + await page.locator('#loadPaste').click(); + + const verdictPeterson = await page.locator('#verdictBadge').textContent(); + assert(verdictPeterson === 'PASS', 'peterson.json renders PASS verdict'); + + // ------------------------------------------------------------- + // Test 6: Load incomplete-only.json (INCOMPLETE verdict) + // ------------------------------------------------------------- + console.log('\nTest 6: Load incomplete-only.json fixture'); + const incompleteJson = readFileSync(join(projectRoot, 'examples/traces/incomplete-only.json'), 'utf8'); + await page.locator('#clearBtn').click(); + await page.locator('#paste').fill(incompleteJson); + await page.locator('#loadPaste').click(); + + const verdictIncomplete = await page.locator('#verdictBadge').textContent(); + assert(verdictIncomplete === 'INCOMPLETE', 'incomplete-only renders INCOMPLETE verdict'); + + // ------------------------------------------------------------- + // Test 7: Program File Load alongside Trace + // ------------------------------------------------------------- + console.log('\nTest 7: Load program file and verify invariant'); + await page.locator('#clearBtn').click(); + await page.locator('#paste').fill(lostUpdateJson); + await page.locator('#loadPaste').click(); + + // Set program file input + const programPath = join(projectRoot, 'src/main/resources/programs/lost-update.json'); + await page.locator('#programFile').setInputFiles(programPath); + + await page.waitForFunction(() => document.querySelector('#stateStrip')?.textContent.includes('Invariant:'), { timeout: 3000 }); + const stripText = await page.locator('#stateStrip').textContent(); + assert(stripText.includes('Invariant:'), 'State strip renders Invariant header when program is loaded'); + + // ------------------------------------------------------------- + // Test 8: Integrity & Console Sanity + // ------------------------------------------------------------- + console.log('\nTest 8: Console and error integrity'); + assert(consoleErrors.length === 0, `Zero console errors or exceptions (found ${consoleErrors.length}: ${consoleErrors.join(', ')})`); + + } finally { + await browser.close(); + await new Promise((resolve) => server.close(resolve)); + } + + console.log(`\nResults: ${passed} passed, ${failed} failed`); + if (failed > 0) { + process.exit(1); + } +} + +runTests().catch((err) => { + console.error('Fatal test error:', err); + process.exit(1); +}); diff --git a/docs/visualizer.css b/docs/visualizer.css index e26267c..a67cbcf 100644 --- a/docs/visualizer.css +++ b/docs/visualizer.css @@ -74,6 +74,7 @@ tr.active-row td:first-child{box-shadow:inset 3px 0 0 var(--accent)} tr.fail-row.active-row{background:var(--fail-bg)} tr.fail-row.active-row td:first-child{box-shadow:inset 3px 0 0 var(--fail)} .cell-active{font-weight:700;border-radius:6px;padding:2px 6px;display:inline-block;border:1px solid transparent} +.val-changed{background:var(--accent-weak);font-weight:700;border-radius:4px;padding:1px 5px;border:1px solid var(--accent);color:var(--text);display:inline-block} .muted{color:var(--muted)} .strip{font:12px var(--mono)} .strip table th,.strip table td{font-family:var(--mono);font-size:12px} diff --git a/docs/visualizer.js b/docs/visualizer.js index e499037..b62dddc 100644 --- a/docs/visualizer.js +++ b/docs/visualizer.js @@ -89,6 +89,57 @@ function capName(s){ return t.length > MAX_NAME_LEN ? t.slice(0, MAX_NAME_LEN) + '…' : t; } +/** + * Compare two state values for equality (handles primitives and shallow arrays/objects). + * @param {*} v1 - first value + * @param {*} v2 - second value + * @returns {boolean} true if equal + */ +function isValEqual(v1, v2){ + if(v1 === v2) return true; + if(v1 == null || v2 == null) return false; + if(Array.isArray(v1) && Array.isArray(v2)){ + if(v1.length !== v2.length) return false; + return v1.every((x, i) => isValEqual(x, v2[i])); + } + if(typeof v1 === 'object' && typeof v2 === 'object'){ + return JSON.stringify(v1) === JSON.stringify(v2); + } + return false; +} + +/** + * Format a snapshot value for safe display. + * @param {*} v - value to format + * @returns {string} formatted string + */ +function formatVal(v){ + if(v === undefined) return '—'; + if(v === null) return 'null'; + if(typeof v === 'boolean') return String(v); + if(typeof v === 'number') return String(v); + if(Array.isArray(v)) return '[' + v.map(formatVal).join(', ') + ']'; + if(typeof v === 'object') return capStr(JSON.stringify(v)); + return capStr(String(v)); +} + +/** + * Render a table cell for a snapshot value, adding .val-changed if it changed from previous config. + * @param {*} val - value at selected config + * @param {boolean} isChanged - whether value changed from previous config + * @returns {HTMLTableCellElement} table cell + */ +function renderValCell(val, isChanged){ + const td = document.createElement('td'); + const span = document.createElement('span'); + span.textContent = formatVal(val); + if(isChanged){ + span.className = 'val-changed'; + } + td.append(span); + return td; +} + /** * Normalize any supported raw JSON payload into a {trace, meta} pair. * Supports TraceRecord {threads}, ReportWriter {benchmarks}, and TestResult @@ -110,7 +161,7 @@ function normalize(raw){ if(ft){ const threads = ft.threads || ft.threadIds; if(!Array.isArray(threads)) throw new Error('benchmarks[].failingTrace missing threads/threadIds'); - return { trace: { threads, outcomes: ft.outcomes, outcome: entry.verdict || 'VIOLATION', programHash: entry.bug }, meta: { verdict: entry.verdict, strategy: entry.strategy, storeType: entry.storeType, statesExplored: entry.statesExplored, wallTimeMs: entry.wallTimeMs, heapDeltaBytes: entry.heapDeltaBytes, bug: entry.bug } }; + return { trace: { threads, outcomes: ft.outcomes, outcome: entry.verdict || 'VIOLATION', programHash: entry.bug, states: ft.states }, meta: { verdict: entry.verdict, strategy: entry.strategy, storeType: entry.storeType, statesExplored: entry.statesExplored, wallTimeMs: entry.wallTimeMs, heapDeltaBytes: entry.heapDeltaBytes, bug: entry.bug } }; } return { trace: { threads: [], outcome: entry.verdict || 'PASS', programHash: entry.bug }, meta: { verdict: entry.verdict, strategy: entry.strategy, storeType: entry.storeType, statesExplored: entry.statesExplored, wallTimeMs: entry.wallTimeMs, heapDeltaBytes: entry.heapDeltaBytes, bug: entry.bug } }; } @@ -380,10 +431,10 @@ function renderStateStrip(){ const el = $('#stateStrip'); el.textContent = ''; - // Snapshot block is independent of programDef (fix 4116389768) const snapshot = currentTrace.states && Array.isArray(currentTrace.states) ? currentTrace.states[selectedIdx] : null; + const prevSnapshot = currentTrace.states && Array.isArray(currentTrace.states) && selectedIdx > 0 ? currentTrace.states[selectedIdx - 1] : null; - if(!programDef){ + if(!programDef && !snapshot){ const p = document.createElement('p'); p.className='placeholder'; p.append(document.createTextNode('No program JSON loaded — load a program file (e.g. ')); const code = document.createElement('code'); code.textContent='src/main/resources/programs/lost-update.json'; @@ -396,35 +447,24 @@ function renderStateStrip(){ p.append(c3); p.append(document.createTextNode(' header. State values are schedule-only today.')); el.append(p); - if(snapshot){ - const ps = document.createElement('p'); ps.className='placeholder'; ps.textContent='Snapshot present for this config (future harness):'; - const pre = document.createElement('pre'); pre.style.font='12px var(--mono)'; pre.style.background='var(--bg)'; pre.style.padding='8px'; pre.style.borderRadius='8px'; pre.style.overflow='auto'; - pre.textContent = JSON.stringify(snapshot, null, 2); - el.append(ps, pre); - } return; } - const fieldsRaw = programDef.state?.fields || (programDef.state?.type ? [{name: programDef.state.type, type: 'typed'}] : []); - const localsRaw = programDef.state?.locals || []; - // Cap display (fix 4116389773) — validated length already ≤MAX_FIELDS, but slice defensively - const fields = Array.isArray(fieldsRaw) ? fieldsRaw.slice(0, MAX_FIELDS) : []; - const locals = Array.isArray(localsRaw) ? localsRaw.slice(0, MAX_FIELDS) : []; - const truncatedFields = Array.isArray(fieldsRaw) && fieldsRaw.length > MAX_FIELDS; - const truncatedLocals = Array.isArray(localsRaw) && localsRaw.length > MAX_FIELDS; - - const div = document.createElement('div'); div.style.marginBottom='8px'; - div.append(document.createTextNode('Invariant: ')); - if(programDef.invariant){ - const code = document.createElement('code'); - code.textContent = capStr(programDef.invariant.expr || JSON.stringify(programDef.invariant)); - div.append(code); - } else { - const sp = document.createElement('span'); sp.className='muted'; sp.textContent='—'; - div.append(sp); + + if(programDef){ + const div = document.createElement('div'); div.style.marginBottom='8px'; + div.append(document.createTextNode('Invariant: ')); + if(programDef.invariant){ + const code = document.createElement('code'); + code.textContent = capStr(programDef.invariant.expr || JSON.stringify(programDef.invariant)); + div.append(code); + } else { + const sp = document.createElement('span'); sp.className='muted'; sp.textContent='—'; + div.append(sp); + } + const wh = document.createElement('span'); wh.className='muted'; wh.textContent = ` (${programDef.invariant?.when||'final'})`; + div.append(wh); + el.append(div); } - const wh = document.createElement('span'); wh.className='muted'; wh.textContent = ` (${programDef.invariant?.when||'final'})`; - div.append(wh); - el.append(div); const table = document.createElement('table'); const thead = document.createElement('thead'); @@ -432,45 +472,141 @@ function renderStateStrip(){ ['Scope','Name','Value at selected config'].forEach(t=>{ const th=document.createElement('th'); th.textContent=t; hr.append(th); }); thead.append(hr); table.append(thead); const tbody = document.createElement('tbody'); - if(fields.length===0 && locals.length===0){ - const tr=document.createElement('tr'); const td=document.createElement('td'); td.colSpan=3; td.className='placeholder'; td.textContent='No fields/locals declared in program JSON.'; tr.append(td); tbody.append(tr); - } else { - fields.forEach(f=>{ - const tr=document.createElement('tr'); - const tdS=document.createElement('td'); tdS.textContent='field'; - const tdN=document.createElement('td'); - const code=document.createElement('code'); code.textContent=capName(String(f.name)); - tdN.append(code); - const mut=document.createElement('span'); mut.className='muted'; mut.textContent=' ' + capName(String(f.type||'')); - tdN.append(mut); - const tdV=document.createElement('td'); tdV.className='placeholder'; tdV.textContent='no snapshot — schedule only (header from program JSON)'; - tr.append(tdS, tdN, tdV); tbody.append(tr); - }); - if(truncatedFields){ - const tr=document.createElement('tr'); const td=document.createElement('td'); td.colSpan=3; td.className='placeholder'; td.textContent=`… truncated, ${fieldsRaw.length - MAX_FIELDS} more fields not shown`; tr.append(td); tbody.append(tr); + + if(snapshot){ + let rowCount = 0; + const fieldMap = new Map(); + if(snapshot.fields && typeof snapshot.fields === 'object' && !Array.isArray(snapshot.fields)){ + for(const [k, v] of Object.entries(snapshot.fields)){ + fieldMap.set(k, v); + } } - locals.forEach(l=>{ - const tr=document.createElement('tr'); - const tdS=document.createElement('td'); tdS.textContent='local'; - const tdN=document.createElement('td'); - const code=document.createElement('code'); code.textContent=capName(String(l.name)); + const declaredFieldTypes = new Map(); + if(programDef && Array.isArray(programDef.state?.fields)){ + programDef.state.fields.forEach(f=>{ if(f && f.name) declaredFieldTypes.set(f.name, f.type); }); + } + + fieldMap.forEach((val, name)=>{ + if(rowCount >= MAX_FIELDS) return; + rowCount++; + const tr = document.createElement('tr'); + const tdS = document.createElement('td'); tdS.textContent = 'field'; + const tdN = document.createElement('td'); + const code = document.createElement('code'); code.textContent = capName(String(name)); tdN.append(code); - const mut=document.createElement('span'); mut.className='muted'; mut.textContent=' ' + capName(String(l.type||'')); - tdN.append(mut); - const tdV=document.createElement('td'); tdV.className='placeholder'; tdV.textContent='no snapshot — schedule only'; - tr.append(tdS, tdN, tdV); tbody.append(tr); + const typeStr = declaredFieldTypes.get(name); + if(typeStr){ + const mut = document.createElement('span'); mut.className = 'muted'; mut.textContent = ' ' + capName(String(typeStr)); + tdN.append(mut); + } + const prevVal = prevSnapshot?.fields ? prevSnapshot.fields[name] : undefined; + const isChanged = prevSnapshot != null && prevVal !== undefined && !isValEqual(prevVal, val); + const tdV = renderValCell(val, isChanged); + tr.append(tdS, tdN, tdV); + tbody.append(tr); }); - if(truncatedLocals){ - const tr=document.createElement('tr'); const td=document.createElement('td'); td.colSpan=3; td.className='placeholder'; td.textContent=`… truncated, ${localsRaw.length - MAX_FIELDS} more locals not shown`; tr.append(td); tbody.append(tr); + + const declaredLocalTypes = new Map(); + if(programDef && Array.isArray(programDef.state?.locals)){ + programDef.state.locals.forEach(l=>{ if(l && l.name) declaredLocalTypes.set(l.name, l.type); }); + } + + if(snapshot.locals && typeof snapshot.locals === 'object' && !Array.isArray(snapshot.locals)){ + const tids = Object.keys(snapshot.locals).sort((a,b)=> { + const na = Number(a), nb = Number(b); + return (!isNaN(na) && !isNaN(nb)) ? na - nb : a.localeCompare(b); + }); + for(const tid of tids){ + const tLocals = snapshot.locals[tid]; + if(!tLocals || typeof tLocals !== 'object' || Array.isArray(tLocals)) continue; + for(const [name, val] of Object.entries(tLocals)){ + if(rowCount >= MAX_FIELDS * 2) break; + rowCount++; + const tr = document.createElement('tr'); + const tdS = document.createElement('td'); tdS.textContent = `local (T${tid})`; + const tdN = document.createElement('td'); + const code = document.createElement('code'); code.textContent = capName(String(name)); + tdN.append(code); + const typeStr = declaredLocalTypes.get(name); + if(typeStr){ + const mut = document.createElement('span'); mut.className = 'muted'; mut.textContent = ' ' + capName(String(typeStr)); + tdN.append(mut); + } + const prevVal = prevSnapshot?.locals?.[tid] ? prevSnapshot.locals[tid][name] : undefined; + const isChanged = prevSnapshot != null && prevVal !== undefined && !isValEqual(prevVal, val); + const tdV = renderValCell(val, isChanged); + tr.append(tdS, tdN, tdV); + tbody.append(tr); + } + } + } + + if(rowCount === 0){ + const tr = document.createElement('tr'); + const td = document.createElement('td'); td.colSpan = 3; td.className = 'placeholder'; + td.textContent = 'Empty state snapshot.'; + tr.append(td); + tbody.append(tr); + } + } else { + // Schedule only — no snapshot + const fieldsRaw = programDef.state?.fields || (programDef.state?.type ? [{name: programDef.state.type, type: 'typed'}] : []); + const localsRaw = programDef.state?.locals || []; + const fields = Array.isArray(fieldsRaw) ? fieldsRaw.slice(0, MAX_FIELDS) : []; + const locals = Array.isArray(localsRaw) ? localsRaw.slice(0, MAX_FIELDS) : []; + const truncatedFields = Array.isArray(fieldsRaw) && fieldsRaw.length > MAX_FIELDS; + const truncatedLocals = Array.isArray(localsRaw) && localsRaw.length > MAX_FIELDS; + + if(fields.length === 0 && locals.length === 0){ + const tr = document.createElement('tr'); + const td = document.createElement('td'); td.colSpan = 3; td.className = 'placeholder'; + td.textContent = 'No fields/locals declared in program JSON.'; + tr.append(td); + tbody.append(tr); + } else { + fields.forEach(f=>{ + const tr = document.createElement('tr'); + const tdS = document.createElement('td'); tdS.textContent = 'field'; + const tdN = document.createElement('td'); + const code = document.createElement('code'); code.textContent = capName(String(f.name)); + tdN.append(code); + const mut = document.createElement('span'); mut.className = 'muted'; mut.textContent = ' ' + capName(String(f.type || '')); + tdN.append(mut); + const tdV = document.createElement('td'); tdV.className = 'placeholder'; tdV.textContent = 'no snapshot — schedule only (header from program JSON)'; + tr.append(tdS, tdN, tdV); + tbody.append(tr); + }); + if(truncatedFields){ + const tr = document.createElement('tr'); + const td = document.createElement('td'); td.colSpan = 3; td.className = 'placeholder'; + td.textContent = `… truncated, ${fieldsRaw.length - MAX_FIELDS} more fields not shown`; + tr.append(td); + tbody.append(tr); + } + locals.forEach(l=>{ + const tr = document.createElement('tr'); + const tdS = document.createElement('td'); tdS.textContent = 'local'; + const tdN = document.createElement('td'); + const code = document.createElement('code'); code.textContent = capName(String(l.name)); + tdN.append(code); + const mut = document.createElement('span'); mut.className = 'muted'; mut.textContent = ' ' + capName(String(l.type || '')); + tdN.append(mut); + const tdV = document.createElement('td'); tdV.className = 'placeholder'; tdV.textContent = 'no snapshot — schedule only'; + tr.append(tdS, tdN, tdV); + tbody.append(tr); + }); + if(truncatedLocals){ + const tr = document.createElement('tr'); + const td = document.createElement('td'); td.colSpan = 3; td.className = 'placeholder'; + td.textContent = `… truncated, ${localsRaw.length - MAX_FIELDS} more locals not shown`; + tr.append(td); + tbody.append(tr); + } } } - table.append(tbody); el.append(table); - if(snapshot){ - const p=document.createElement('p'); p.className='placeholder'; p.textContent='Snapshot present for this config (future harness):'; - const pre=document.createElement('pre'); pre.style.font='12px var(--mono)'; pre.style.background='var(--bg)'; pre.style.padding='8px'; pre.style.borderRadius='8px'; pre.style.overflow='auto'; - pre.textContent = JSON.stringify(snapshot, null, 2); - el.append(p, pre); - } + + table.append(tbody); + el.append(table); } /** @@ -551,7 +687,21 @@ copyBtn.addEventListener('click', async ()=>{ }); const samples = { - 'lost-update': { trace: { threads:[0,1,0,1], outcomes:["ADVANCED","ADVANCED","ADVANCED","ADVANCED"], outcome:"VIOLATION" }, meta:{verdict:"VIOLATION", bug:"lost-update", strategy:"DFS", storeType:"EXACT", statesExplored:13} }, + 'lost-update': { + trace: { + threads: [0, 1, 0, 1], + outcomes: ["ADVANCED", "ADVANCED", "ADVANCED", "ADVANCED"], + outcome: "VIOLATION", + states: [ + {"fields": {"counter": 0, "control": false}, "locals": {"0": {"register": 0}, "1": {"register": 0}}}, + {"fields": {"counter": 0, "control": false}, "locals": {"0": {"register": 0}, "1": {"register": 0}}}, + {"fields": {"counter": 0, "control": false}, "locals": {"0": {"register": 0}, "1": {"register": 0}}}, + {"fields": {"counter": 1, "control": true}, "locals": {"0": {"register": 0}, "1": {"register": 0}}}, + {"fields": {"counter": 1, "control": true}, "locals": {"0": {"register": 0}, "1": {"register": 0}}} + ] + }, + meta: {verdict: "VIOLATION", bug: "lost-update", strategy: "DFS", storeType: "EXACT", statesExplored: 13} + }, 'peterson': { trace: { threads:[], outcome:"PASS" }, meta:{verdict:"PASS", bug:"peterson", strategy:"DFS", storeType:"EXACT", statesExplored:6} }, 'bounded-buffer': { trace: { threads:[], outcome:"PASS" }, meta:{verdict:"PASS", bug:"bounded-buffer-declarative", strategy:"DFS", storeType:"EXACT", statesExplored:6} } }; diff --git a/examples/traces/lost-update.json b/examples/traces/lost-update.json index 8dc4fa0..bb201be 100644 --- a/examples/traces/lost-update.json +++ b/examples/traces/lost-update.json @@ -9,7 +9,14 @@ "heapDeltaBytes": 848376, "failingTrace": { "threadIds": [0, 1, 0, 1], - "outcomes": ["ADVANCED", "ADVANCED", "ADVANCED", "ADVANCED"] + "outcomes": ["ADVANCED", "ADVANCED", "ADVANCED", "ADVANCED"], + "states": [ + {"fields": {"counter": 0, "control": false}, "locals": {"0": {"register": 0}, "1": {"register": 0}}}, + {"fields": {"counter": 0, "control": false}, "locals": {"0": {"register": 0}, "1": {"register": 0}}}, + {"fields": {"counter": 0, "control": false}, "locals": {"0": {"register": 0}, "1": {"register": 0}}}, + {"fields": {"counter": 1, "control": true}, "locals": {"0": {"register": 0}, "1": {"register": 0}}}, + {"fields": {"counter": 1, "control": true}, "locals": {"0": {"register": 0}, "1": {"register": 0}}} + ] }, "verdict": "VIOLATION" } diff --git a/src/main/java/dev/samhb/interleave/InterleaveRunner.java b/src/main/java/dev/samhb/interleave/InterleaveRunner.java index 921e25a..f96309e 100644 --- a/src/main/java/dev/samhb/interleave/InterleaveRunner.java +++ b/src/main/java/dev/samhb/interleave/InterleaveRunner.java @@ -2,8 +2,9 @@ package dev.samhb.interleave; import dev.samhb.interleave.cb.ContextBoundedExplorer; -import dev.samhb.interleave.core.Program; import dev.samhb.interleave.core.Configuration; +import dev.samhb.interleave.core.Program; +import dev.samhb.interleave.core.StateSnapshot; import dev.samhb.interleave.search.*; import dev.samhb.interleave.dpor.DporExplorer; import dev.samhb.interleave.por.StaticPorExplorer; @@ -104,7 +105,7 @@ TestResult run(Program program, LongSupplier clock) { }; LimitState limitState = new LimitState(); - StateVisitor visitor = createLimitEnforcingVisitor(limitState, clock); + StateVisitor visitor = createLimitEnforcingVisitor(limitState, clock, program); DfsResult result; try { @@ -142,7 +143,7 @@ TestResult run(Program program, LongSupplier clock) { long wallTime = clock.getAsLong() - start; long heapDelta = Math.max(0, memAfter - memBefore); - return convertToTestResult(result, wallTime, heapDelta, false); + return convertToTestResult(result, program, wallTime, heapDelta, false); } /** @@ -151,9 +152,10 @@ TestResult run(Program program, LongSupplier clock) { * after updating the partial count, so the visit that reaches a limit is included. * @param limitState run-local counters and interruption state * @param clock per-call millisecond clock used to enforce the configured deadline + * @param program program whose steps are replayed for snapshot enrichment * @return visitor sharing the supplied run-local limit counters and captured traces */ - private StateVisitor createLimitEnforcingVisitor(LimitState limitState, LongSupplier clock) { + private StateVisitor createLimitEnforcingVisitor(LimitState limitState, LongSupplier clock, Program program) { long[] stateCount = {0}; long startTime = clock.getAsLong(); @@ -196,6 +198,14 @@ public void onStateVisited(Configuration config) { @Override public void onTraceCreated(Trace trace) { TraceRecord record = trace.toRecord(); + if (program != null) { + try { + List states = new TraceReplayer().captureSnapshots(program, trace); + record = record.withStates(states); + } catch (Exception ignored) { + // Diagnostic snapshot enrichment is best-effort + } + } limitState.partialResult = limitState.partialResult.withTrace(record); } }; @@ -377,22 +387,44 @@ private static boolean isFailure(DfsResult result) { /** * Converts exploration counts and trace categories into the public result format. * @param result completed exploration result + * @param program program whose steps were explored * @param wallTime elapsed exploration time in milliseconds * @param heapDelta observed heap delta in bytes * @param limitExceeded whether a configured exploration limit stopped the run * @return public result preserving counts, categorized traces, and the interruption flag */ - private TestResult convertToTestResult(DfsResult result, long wallTime, long heapDelta, boolean limitExceeded) { + private TestResult convertToTestResult(DfsResult result, Program program, long wallTime, long heapDelta, boolean limitExceeded) { List failingTraces = new ArrayList<>(); List deadlockedTraces = new ArrayList<>(); List completedTraces = new ArrayList<>(); List incompleteTraces = new ArrayList<>(); + TraceReplayer replayer = new TraceReplayer(); for (Trace trace : result.traces()) { TraceRecord record = trace.toRecord(); switch (trace.outcome()) { - case VIOLATION -> failingTraces.add(record); - case DEADLOCK -> deadlockedTraces.add(record); + case VIOLATION -> { + if (program != null) { + try { + List states = replayer.captureSnapshots(program, trace); + record = record.withStates(states); + } catch (Exception ignored) { + // Diagnostic snapshot capture is best-effort + } + } + failingTraces.add(record); + } + case DEADLOCK -> { + if (program != null) { + try { + List states = replayer.captureSnapshots(program, trace); + record = record.withStates(states); + } catch (Exception ignored) { + // Diagnostic snapshot capture is best-effort + } + } + deadlockedTraces.add(record); + } case COMPLETED -> completedTraces.add(record); case INCOMPLETE -> incompleteTraces.add(record); } diff --git a/src/main/java/dev/samhb/interleave/TraceRecord.java b/src/main/java/dev/samhb/interleave/TraceRecord.java index 6f7d510..d5e2947 100644 --- a/src/main/java/dev/samhb/interleave/TraceRecord.java +++ b/src/main/java/dev/samhb/interleave/TraceRecord.java @@ -3,6 +3,7 @@ import com.google.gson.Gson; import com.google.gson.GsonBuilder; +import dev.samhb.interleave.core.StateSnapshot; import dev.samhb.interleave.core.StepOutcome; import dev.samhb.interleave.search.TraceOutcome; import java.io.Serializable; @@ -20,6 +21,8 @@ public final class TraceRecord implements Serializable { private final TraceOutcome outcome; /** Program hash. */ private final String programHash; + /** State snapshots. */ + private final List states; /** * Creates trace record from the supplied values. @@ -29,10 +32,23 @@ public final class TraceRecord implements Serializable { * @param programHash diagnostic program fingerprint, if available */ public TraceRecord(List threadIds, List outcomes, TraceOutcome outcome, String programHash) { + this(threadIds, outcomes, outcome, programHash, List.of()); + } + + /** + * Creates trace record from the supplied values, including execution state snapshots. + * @param threadIds ordered thread choices in the trace + * @param outcomes outcome of each recorded step + * @param outcome execution outcome being recorded + * @param programHash diagnostic program fingerprint, if available + * @param states ordered state snapshots along the execution path + */ + public TraceRecord(List threadIds, List outcomes, TraceOutcome outcome, String programHash, List states) { this.threadIds = List.copyOf(threadIds); this.outcomes = List.copyOf(outcomes); this.outcome = outcome; this.programHash = programHash; + this.states = states == null ? List.of() : List.copyOf(states); } /** @@ -68,7 +84,25 @@ public String programHash() { } /** - * Serializes thread choices, step outcomes, terminal verdict, and the optional program fingerprint. + * Returns ordered execution state snapshots, if captured. + * @return immutable ordered state snapshots + */ + public List states() { + return states; + } + + /** + * Returns a copy of this trace record enriched with the supplied state snapshots. + * @param states state snapshots along the execution path + * @return enriched trace record + */ + public TraceRecord withStates(List states) { + return new TraceRecord(this.threadIds, this.outcomes, this.outcome, this.programHash, states); + } + + /** + * Serializes thread choices, step outcomes, terminal verdict, the optional program fingerprint, + * and optional state snapshots. * @return JSON containing this result’s recorded values */ public String toJson() { @@ -87,8 +121,11 @@ public String toJson() { } sb.append("],\n"); sb.append(" \"outcome\": \"").append(outcome).append("\",\n"); - sb.append(" \"programHash\": ").append(GSON.toJson(programHash)).append("\n"); - sb.append("}"); + sb.append(" \"programHash\": ").append(GSON.toJson(programHash)); + if (!states.isEmpty()) { + sb.append(",\n \"states\": ").append(GSON.toJson(states)); + } + sb.append("\n}"); return sb.toString(); } } diff --git a/src/main/java/dev/samhb/interleave/core/CounterState.java b/src/main/java/dev/samhb/interleave/core/CounterState.java index 4e06f02..5e705a7 100644 --- a/src/main/java/dev/samhb/interleave/core/CounterState.java +++ b/src/main/java/dev/samhb/interleave/core/CounterState.java @@ -109,6 +109,14 @@ public int getRegister(int threadId) { return registers[threadId]; } + /** + * Returns the number of thread-local registers modeled by this state. + * @return register and thread count + */ + public int threadCount() { + return registers.length; + } + /** * Sets thread-local register. * @param threadId thread id diff --git a/src/main/java/dev/samhb/interleave/core/DeadlockState.java b/src/main/java/dev/samhb/interleave/core/DeadlockState.java index 61430d9..0675c13 100644 --- a/src/main/java/dev/samhb/interleave/core/DeadlockState.java +++ b/src/main/java/dev/samhb/interleave/core/DeadlockState.java @@ -52,6 +52,14 @@ public boolean flag(int threadId) { return flag[threadId]; } + /** + * Returns the number of threads modeled by this state. + * @return thread count + */ + public int threadCount() { + return flag.length; + } + /** * Updates flag in this mutable modeled state. * @param threadId zero-based modeled thread ID diff --git a/src/main/java/dev/samhb/interleave/core/StateSnapshot.java b/src/main/java/dev/samhb/interleave/core/StateSnapshot.java new file mode 100644 index 0000000..1d2c295 --- /dev/null +++ b/src/main/java/dev/samhb/interleave/core/StateSnapshot.java @@ -0,0 +1,68 @@ +/** Immutable snapshot of state variables at a specific execution configuration. */ +package dev.samhb.interleave.core; + +import java.io.Serializable; +import java.util.Collections; +import java.util.LinkedHashMap; +import java.util.Map; + +/** + * Immutable snapshot of state variables at a specific execution configuration. + * + *

Captures shared fields and per-thread local variables for inspection, trace replay, + * and visualizer rendering. + * + * @param fields map of field names to values (scalars, boolean/integer arrays) + * @param locals map of thread id strings (e.g. "0", "1") to maps of local names and values + */ +public record StateSnapshot( + Map fields, + Map> locals +) implements Serializable { + + /** + * Compact constructor enforcing deep immutability by copying nested maps and cloning arrays. + */ + public StateSnapshot { + fields = deepCopyFields(fields); + locals = deepCopyLocals(locals); + } + + private static Map deepCopyFields(Map map) { + if (map == null || map.isEmpty()) { + return Map.of(); + } + Map copy = new LinkedHashMap<>(); + for (Map.Entry entry : map.entrySet()) { + Object val = entry.getValue(); + if (val instanceof int[] arr) { + val = arr.clone(); + } else if (val instanceof boolean[] arr) { + val = arr.clone(); + } + copy.put(entry.getKey(), val); + } + return Collections.unmodifiableMap(copy); + } + + private static Map> deepCopyLocals(Map> map) { + if (map == null || map.isEmpty()) { + return Map.of(); + } + Map> copy = new LinkedHashMap<>(); + for (Map.Entry> entry : map.entrySet()) { + copy.put(entry.getKey(), deepCopyFields(entry.getValue())); + } + return Collections.unmodifiableMap(copy); + } + + /** + * Factory for snapshots with fields only. + * + * @param fields field mapping + * @return snapshot with empty locals + */ + public static StateSnapshot ofFields(Map fields) { + return new StateSnapshot(fields, Map.of()); + } +} diff --git a/src/main/java/dev/samhb/interleave/core/StateSnapshotExtractor.java b/src/main/java/dev/samhb/interleave/core/StateSnapshotExtractor.java new file mode 100644 index 0000000..1a2475a --- /dev/null +++ b/src/main/java/dev/samhb/interleave/core/StateSnapshotExtractor.java @@ -0,0 +1,127 @@ +/** Extracts immutable state snapshots from any shared state implementation. */ +package dev.samhb.interleave.core; + +import dev.samhb.interleave.format.dsl.DynamicState; +import dev.samhb.interleave.format.dsl.FieldDecl; +import dev.samhb.interleave.format.dsl.LocalDecl; +import java.util.LinkedHashMap; +import java.util.Map; + +/** + * Extracts immutable state snapshots from any {@link SharedState} implementation. + */ +public final class StateSnapshotExtractor { + + private StateSnapshotExtractor() {} + + /** + * Extracts an immutable snapshot from the given shared state. + * + * @param state the state to snapshot + * @return an immutable snapshot of the state's fields and locals + */ + public static StateSnapshot extract(SharedState state) { + if (state instanceof DynamicState ds) { + return extractDynamic(ds); + } else if (state instanceof PetersonState ps) { + return extractPeterson(ps); + } else if (state instanceof CounterState cs) { + return extractCounter(cs); + } else if (state instanceof PairState ps) { + return extractPair(ps); + } else if (state instanceof DeadlockState ds) { + return extractDeadlock(ds); + } else if (state instanceof DclState ds) { + return extractDcl(ds); + } else { + return StateSnapshot.ofFields(Map.of()); + } + } + + private static StateSnapshot extractDynamic(DynamicState ds) { + Map fields = new LinkedHashMap<>(); + for (FieldDecl f : ds.decl().fields()) { + String name = f.name(); + switch (f.type()) { + case INT -> fields.put(name, ds.getInt(name)); + case BOOL -> fields.put(name, ds.getBool(name)); + case INT_ARRAY -> fields.put(name, ds.getArray(name)); + } + } + + Map> locals = new LinkedHashMap<>(); + for (int tid = 0; tid < ds.threadCount(); tid++) { + Map threadLocals = new LinkedHashMap<>(); + for (LocalDecl l : ds.decl().locals()) { + String name = l.name(); + switch (l.type()) { + case INT -> threadLocals.put(name, ds.getLocalInt(tid, name)); + case BOOL -> threadLocals.put(name, ds.getLocalBool(tid, name)); + case INT_ARRAY -> threadLocals.put(name, ds.getLocalArray(tid, name)); + } + } + if (!threadLocals.isEmpty()) { + locals.put(String.valueOf(tid), threadLocals); + } + } + + return new StateSnapshot(fields, locals); + } + + private static StateSnapshot extractPeterson(PetersonState ps) { + Map fields = new LinkedHashMap<>(); + boolean[] flags = new boolean[ps.threadCount()]; + for (int i = 0; i < ps.threadCount(); i++) { + flags[i] = ps.flag(i); + } + fields.put("flag", flags); + fields.put("turn", ps.turn()); + fields.put("inCriticalSection", ps.inCriticalSection()); + return StateSnapshot.ofFields(fields); + } + + private static StateSnapshot extractCounter(CounterState cs) { + Map fields = new LinkedHashMap<>(); + fields.put("counter", cs.counter()); + fields.put("control", cs.control()); + + Map> locals = new LinkedHashMap<>(); + for (int i = 0; i < cs.threadCount(); i++) { + locals.put(String.valueOf(i), Map.of("register", cs.getRegister(i))); + } + return new StateSnapshot(fields, locals); + } + + private static StateSnapshot extractPair(PairState ps) { + Map fields = new LinkedHashMap<>(); + fields.put("high", ps.high()); + fields.put("low", ps.low()); + fields.put("control", ps.control()); + fields.put("observedHigh", ps.observedHigh()); + fields.put("observedLow", ps.observedLow()); + fields.put("hasObservation", ps.hasObservation()); + return StateSnapshot.ofFields(fields); + } + + private static StateSnapshot extractDeadlock(DeadlockState ds) { + Map fields = new LinkedHashMap<>(); + boolean[] flags = new boolean[ds.threadCount()]; + for (int i = 0; i < ds.threadCount(); i++) { + flags[i] = ds.flag(i); + } + fields.put("flag", flags); + fields.put("control", ds.control()); + return StateSnapshot.ofFields(fields); + } + + private static StateSnapshot extractDcl(DclState ds) { + Map fields = new LinkedHashMap<>(); + fields.put("initialized", ds.initialized()); + fields.put("instance", ds.instance() == null ? "null" : String.valueOf(ds.instance())); + fields.put("locked", ds.locked()); + fields.put("lockOwner", ds.lockOwner()); + fields.put("control", ds.control()); + fields.put("observedInstance", ds.observedInstance() == null ? "null" : String.valueOf(ds.observedInstance())); + return StateSnapshot.ofFields(fields); + } +} diff --git a/src/main/java/dev/samhb/interleave/report/BenchmarkHarness.java b/src/main/java/dev/samhb/interleave/report/BenchmarkHarness.java index 863ddfa..bce8c1e 100644 --- a/src/main/java/dev/samhb/interleave/report/BenchmarkHarness.java +++ b/src/main/java/dev/samhb/interleave/report/BenchmarkHarness.java @@ -10,11 +10,12 @@ import dev.samhb.interleave.search.DfsExplorer; import dev.samhb.interleave.search.DfsResult; import dev.samhb.interleave.search.Invariant; +import dev.samhb.interleave.search.StateStore; import dev.samhb.interleave.search.Trace; import dev.samhb.interleave.search.TraceOutcome; +import dev.samhb.interleave.search.TraceReplayer; import dev.samhb.interleave.state.BitstateStore; import dev.samhb.interleave.state.HashingStateStore; -import dev.samhb.interleave.search.StateStore; import java.util.*; /** @@ -180,7 +181,7 @@ private List runProgramWithStore(BenchmarkProgram program, Inva " for " + program.name() + " but got " + dfsVerdict); } Trace dfsFailing = findFailingTrace(dfsResult.result()); - results.add(createResult("DFS", program.name(), dfsResult, dfsVerdict, dfsFailing, storeType, dfsStore, null)); + results.add(createResult("DFS", program.name(), program.program(), dfsResult, dfsVerdict, dfsFailing, storeType, dfsStore, null)); } // STATIC_POR @@ -190,7 +191,7 @@ private List runProgramWithStore(BenchmarkProgram program, Inva DfsResultWithTiming porResult = runExplorer(() -> porExplorer.explore(program.program(), invariant, porStore, null)); String porVerdict = actualVerdict(porResult.result()); Trace porFailing = findFailingTrace(porResult.result()); - results.add(createResult("STATIC_POR", program.name(), porResult, porVerdict, porFailing, storeType, porStore, null)); + results.add(createResult("STATIC_POR", program.name(), program.program(), porResult, porVerdict, porFailing, storeType, porStore, null)); } // DPOR @@ -200,7 +201,7 @@ private List runProgramWithStore(BenchmarkProgram program, Inva DfsResultWithTiming dporResult = runExplorer(() -> dporExplorer.explore(program.program(), invariant, dporStore, null)); String dporVerdict = actualVerdict(dporResult.result()); Trace dporFailing = findFailingTrace(dporResult.result()); - results.add(createResult("DPOR", program.name(), dporResult, dporVerdict, dporFailing, storeType, dporStore, null)); + results.add(createResult("DPOR", program.name(), program.program(), dporResult, dporVerdict, dporFailing, storeType, dporStore, null)); } // CONTEXT_BOUNDED @@ -215,7 +216,7 @@ private List runProgramWithStore(BenchmarkProgram program, Inva // The store that actually produced this result, not the pre-branch one: under // iterative deepening the winning iteration used its own store, and the Bloom metrics // must describe that one rather than an unsearched instance. - results.add(createResult(CONTEXT_BOUNDED, program.name(), result, verdict, failing, + results.add(createResult(CONTEXT_BOUNDED, program.name(), program.program(), result, verdict, failing, storeType, cbRun.store(), cbRun.preemptionsUsed())); } @@ -311,23 +312,32 @@ private static boolean isFailure(DfsResult result) { * @param verdict reported exploration verdict * @param failingTrace representative failure trace, or null when absent * @param storeType visited-store strategy represented by this row + * @param program program whose steps were explored * @param store visited-position store for this run * @param preemptionsUsed preemption bound used, or null for an unbounded strategy * @return benchmark row preserving verdict, trace, measurements, and store diagnostics */ - private BenchmarkResult createResult(String strategy, String bugName, + private BenchmarkResult createResult(String strategy, String bugName, Program program, DfsResultWithTiming result, String verdict, Trace failingTrace, StoreType storeType, StateStore store, Integer preemptionsUsed) { + List states = List.of(); + if (failingTrace != null && program != null) { + try { + states = new TraceReplayer().captureSnapshots(program, failingTrace); + } catch (Exception e) { + states = List.of(); + } + } if (store instanceof BitstateStore bs) { return new BenchmarkResult(strategy, bugName, result.result().statesExplored(), result.wallTimeMs(), result.heapDeltaBytes(), verdict, failingTrace, storeType, - bs.estimatedFalsePositiveRate(), bs.bitCount(), bs.bitDensity(), preemptionsUsed); + bs.estimatedFalsePositiveRate(), bs.bitCount(), bs.bitDensity(), preemptionsUsed, states); } return new BenchmarkResult(strategy, bugName, result.result().statesExplored(), result.wallTimeMs(), result.heapDeltaBytes(), verdict, - failingTrace, storeType, 0.0, 0, 0.0, preemptionsUsed); + failingTrace, storeType, 0.0, 0, 0.0, preemptionsUsed, states); } /** diff --git a/src/main/java/dev/samhb/interleave/report/BenchmarkResult.java b/src/main/java/dev/samhb/interleave/report/BenchmarkResult.java index d9e2215..a2de6c7 100644 --- a/src/main/java/dev/samhb/interleave/report/BenchmarkResult.java +++ b/src/main/java/dev/samhb/interleave/report/BenchmarkResult.java @@ -1,7 +1,9 @@ /** Immutable result of a single benchmark run (one strategy + one store type). */ package dev.samhb.interleave.report; +import dev.samhb.interleave.core.StateSnapshot; import dev.samhb.interleave.search.Trace; +import java.util.List; import java.util.Optional; /** @@ -32,6 +34,8 @@ public final class BenchmarkResult { private final double bitstateBitDensity; /** Preemptions used. */ private final Integer preemptionsUsed; + /** State snapshots. */ + private final List states; /** * Creates a result with the exact store type (backward compatible). @@ -147,6 +151,33 @@ public BenchmarkResult(String strategy, String bugName, long statesExplored, Trace failingTrace, StoreType storeType, double estimatedFalsePositiveRate, int bitstateBitCount, double bitstateBitDensity, Integer preemptionsUsed) { + this(strategy, bugName, statesExplored, wallTimeMs, heapDeltaBytes, verdict, + failingTrace, storeType, estimatedFalsePositiveRate, bitstateBitCount, + bitstateBitDensity, preemptionsUsed, List.of()); + } + + /** + * Creates a benchmark row with full parameters and state snapshots. + * @param strategy exploration strategy used for these results + * @param bugName benchmark program name + * @param statesExplored number of explored configurations + * @param wallTimeMs elapsed exploration time in milliseconds + * @param heapDeltaBytes observed heap delta in bytes + * @param verdict reported exploration verdict + * @param failingTrace representative failure trace, or null when absent + * @param storeType visited-store strategy represented by this row + * @param estimatedFalsePositiveRate estimated Bloom-filter false-positive rate; zero for an exact store + * @param bitstateBitCount number of set bits in the Bloom filter + * @param bitstateBitDensity fraction of Bloom-filter bits that are set + * @param preemptionsUsed the preemption bound the search actually ran at, or null + * @param states captured state snapshots along the failing trace + */ + public BenchmarkResult(String strategy, String bugName, long statesExplored, + long wallTimeMs, long heapDeltaBytes, String verdict, + Trace failingTrace, StoreType storeType, + double estimatedFalsePositiveRate, int bitstateBitCount, + double bitstateBitDensity, Integer preemptionsUsed, + List states) { this.strategy = strategy; this.bugName = bugName; this.statesExplored = statesExplored; @@ -159,6 +190,7 @@ public BenchmarkResult(String strategy, String bugName, long statesExplored, this.bitstateBitCount = bitstateBitCount; this.bitstateBitDensity = bitstateBitDensity; this.preemptionsUsed = preemptionsUsed; + this.states = states == null ? List.of() : List.copyOf(states); } /** @@ -276,4 +308,12 @@ public double bitstateBitDensity() { public Integer preemptionsUsed() { return preemptionsUsed; } + + /** + * Returns captured state snapshots for the failing trace, if available. + * @return immutable ordered state snapshots + */ + public List states() { + return states; + } } diff --git a/src/main/java/dev/samhb/interleave/report/ReportWriter.java b/src/main/java/dev/samhb/interleave/report/ReportWriter.java index fdc516c..29aa10a 100644 --- a/src/main/java/dev/samhb/interleave/report/ReportWriter.java +++ b/src/main/java/dev/samhb/interleave/report/ReportWriter.java @@ -4,6 +4,7 @@ import com.google.gson.Gson; import com.google.gson.GsonBuilder; import dev.samhb.interleave.bugs.BugCorpus; +import dev.samhb.interleave.core.StateSnapshot; import dev.samhb.interleave.core.StepOutcome; import dev.samhb.interleave.search.Trace; import java.util.*; @@ -89,7 +90,7 @@ public String writeJson() { // Failing trace if (result.failingTrace().isPresent()) { sb.append(" \"failingTrace\": "); - sb.append(formatFailingTrace(result.failingTrace().get())); + sb.append(formatFailingTrace(result.failingTrace().get(), result.states())); sb.append(",\n"); } @@ -129,11 +130,12 @@ private static String formatPreemptions(BenchmarkResult result) { } /** - * Formats recorded thread choices and outcomes for a failure row. + * Formats recorded thread choices, outcomes, and optional state snapshots for a failure row. * @param trace recorded execution to inspect or replay - * @return formatted thread choices and outcomes, or the absent-trace placeholder + * @param states captured state snapshots, if available + * @return formatted thread choices, outcomes, and state snapshots */ - private static String formatFailingTrace(Trace trace) { + private static String formatFailingTrace(Trace trace, List states) { StringBuilder sb = new StringBuilder(); sb.append("{\n"); sb.append(" \"threadIds\": ["); @@ -147,8 +149,11 @@ private static String formatFailingTrace(Trace trace) { if (i > 0) sb.append(", "); sb.append(String.format("\"%s\"", trace.outcomes().get(i))); } - sb.append("]\n"); - sb.append(" }"); + sb.append("]"); + if (states != null && !states.isEmpty()) { + sb.append(",\n \"states\": ").append(GSON.toJson(states)); + } + sb.append("\n }"); return sb.toString(); } diff --git a/src/main/java/dev/samhb/interleave/search/TraceReplayer.java b/src/main/java/dev/samhb/interleave/search/TraceReplayer.java index 8947910..3a7cfe2 100644 --- a/src/main/java/dev/samhb/interleave/search/TraceReplayer.java +++ b/src/main/java/dev/samhb/interleave/search/TraceReplayer.java @@ -1,7 +1,11 @@ /** Reconstructs a configuration from recorded choices and trusted step outcomes. */ package dev.samhb.interleave.search; +import dev.samhb.interleave.TraceRecord; import dev.samhb.interleave.core.*; +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; /** Reconstructs a configuration from recorded choices and trusted step outcomes. */ public final class TraceReplayer { @@ -49,5 +53,58 @@ public Configuration replay(Program program, Trace trace) { return config; } + + /** + * Replays thread choices and captures an immutable state snapshot at each configuration along the path. + * + *

Returns a list of length {@code trace.length() + 1}, starting with the initial configuration's + * snapshot and ending with the terminal configuration's snapshot. + * + * @param program program whose initial state and steps are replayed + * @param trace recorded thread choices and outcomes + * @return ordered list of state snapshots for each configuration from initial to terminal + * @throws CorruptedTraceException if an executed step outcome differs from the trace outcome + * @throws IndexOutOfBoundsException if a recorded thread, counter, or outcome index is invalid + */ + public List captureSnapshots(Program program, Trace trace) { + List snapshots = new ArrayList<>(); + Configuration config = program.initialConfiguration(); + snapshots.add(StateSnapshotExtractor.extract(config.state())); + + for (int i = 0; i < trace.threadIds().size(); i++) { + int threadId = trace.threadIds().get(i); + StepOutcome outcome = trace.outcomes().get(i); + + ModelThread thread = program.threads().get(threadId); + int pc = config.programCounters().get(threadId); + Step step = thread.steps().get(pc); + + StepOutcome actualOutcome = step.execute(config.state()); + if (actualOutcome != outcome) { + throw new CorruptedTraceException( + "Trace outcome mismatch at step " + i + " (thread " + threadId + "): " + + "recorded " + outcome + " but execution produced " + actualOutcome + ); + } + config = config.successor(threadId, outcome, program.threads(), config.state()); + snapshots.add(StateSnapshotExtractor.extract(config.state())); + } + + return Collections.unmodifiableList(snapshots); + } + + /** + * Replays a trace record against the given program and returns an enriched trace record + * containing state snapshots. + * + * @param program program whose steps are replayed + * @param record trace record to enrich + * @return enriched trace record containing captured state snapshots + */ + public TraceRecord enrich(Program program, TraceRecord record) { + Trace trace = Trace.of(record.threadIds(), record.outcomes(), record.outcome()); + List snapshots = captureSnapshots(program, trace); + return record.withStates(snapshots); + } } diff --git a/src/test/java/dev/samhb/interleave/TraceRecordTest.java b/src/test/java/dev/samhb/interleave/TraceRecordTest.java new file mode 100644 index 0000000..6628b52 --- /dev/null +++ b/src/test/java/dev/samhb/interleave/TraceRecordTest.java @@ -0,0 +1,76 @@ +package dev.samhb.interleave; + +import dev.samhb.interleave.core.StateSnapshot; +import dev.samhb.interleave.core.StepOutcome; +import dev.samhb.interleave.search.TraceOutcome; +import org.junit.jupiter.api.Test; + +import java.util.List; +import java.util.Map; + +import static org.junit.jupiter.api.Assertions.*; + +class TraceRecordTest { + + @Test + void constructor4Arg_defaultsStatesToEmpty() { + TraceRecord record = new TraceRecord( + List.of(0, 1), + List.of(StepOutcome.ADVANCED, StepOutcome.ADVANCED), + TraceOutcome.VIOLATION, + "test-hash" + ); + + assertEquals(List.of(0, 1), record.threadIds()); + assertEquals(List.of(StepOutcome.ADVANCED, StepOutcome.ADVANCED), record.outcomes()); + assertEquals(TraceOutcome.VIOLATION, record.outcome()); + assertEquals("test-hash", record.programHash()); + assertTrue(record.states().isEmpty()); + + String json = record.toJson(); + assertFalse(json.contains("\"states\"")); + } + + @Test + void constructor5Arg_serializesStatesInJson() { + StateSnapshot s0 = StateSnapshot.ofFields(Map.of("counter", 0)); + StateSnapshot s1 = StateSnapshot.ofFields(Map.of("counter", 1)); + + TraceRecord record = new TraceRecord( + List.of(0), + List.of(StepOutcome.ADVANCED), + TraceOutcome.COMPLETED, + "test-hash", + List.of(s0, s1) + ); + + assertEquals(2, record.states().size()); + assertEquals(0, record.states().get(0).fields().get("counter")); + assertEquals(1, record.states().get(1).fields().get("counter")); + + String json = record.toJson(); + assertTrue(json.contains("\"states\":")); + assertTrue(json.contains("\"counter\": 0") || json.contains("\"counter\":0")); + assertTrue(json.contains("\"counter\": 1") || json.contains("\"counter\":1")); + } + + @Test + void withStates_createsEnrichedCopy() { + TraceRecord original = new TraceRecord( + List.of(0), + List.of(StepOutcome.ADVANCED), + TraceOutcome.COMPLETED, + "test-hash" + ); + + StateSnapshot snap = StateSnapshot.ofFields(Map.of("x", 42)); + TraceRecord enriched = original.withStates(List.of(snap)); + + assertEquals(original.threadIds(), enriched.threadIds()); + assertEquals(original.outcomes(), enriched.outcomes()); + assertEquals(original.outcome(), enriched.outcome()); + assertEquals(original.programHash(), enriched.programHash()); + assertEquals(1, enriched.states().size()); + assertEquals(42, enriched.states().get(0).fields().get("x")); + } +} diff --git a/src/test/java/dev/samhb/interleave/core/StateSnapshotExtractorTest.java b/src/test/java/dev/samhb/interleave/core/StateSnapshotExtractorTest.java new file mode 100644 index 0000000..14c70a6 --- /dev/null +++ b/src/test/java/dev/samhb/interleave/core/StateSnapshotExtractorTest.java @@ -0,0 +1,153 @@ +package dev.samhb.interleave.core; + +import dev.samhb.interleave.format.dsl.DynamicState; +import dev.samhb.interleave.format.dsl.FieldDecl; +import dev.samhb.interleave.format.dsl.LocalDecl; +import dev.samhb.interleave.format.dsl.StateDecl; +import org.junit.jupiter.api.Test; + +import java.util.List; +import java.util.Map; + +import static org.junit.jupiter.api.Assertions.*; + +class StateSnapshotExtractorTest { + + @Test + void extractDynamic_capturesFieldsAndLocals() { + StateDecl decl = new StateDecl( + List.of( + FieldDecl.ofInt("x", 42), + FieldDecl.ofBool("flag", true), + FieldDecl.ofArray("arr", new int[]{1, 2, 3}) + ), + List.of( + LocalDecl.ofInt("locI", 10), + LocalDecl.ofBool("locB", false), + LocalDecl.ofArray("locA", new int[]{9, 8}) + ) + ); + DynamicState ds = new DynamicState(decl, 2); + ds.setInt("x", 99); + ds.setLocalInt(1, "locI", 77); + + StateSnapshot snapshot = StateSnapshotExtractor.extract(ds); + + assertEquals(99, snapshot.fields().get("x")); + assertEquals(true, snapshot.fields().get("flag")); + assertArrayEquals(new int[]{1, 2, 3}, (int[]) snapshot.fields().get("arr")); + + Map t0Locals = snapshot.locals().get("0"); + assertNotNull(t0Locals); + assertEquals(10, t0Locals.get("locI")); + assertEquals(false, t0Locals.get("locB")); + assertArrayEquals(new int[]{9, 8}, (int[]) t0Locals.get("locA")); + + Map t1Locals = snapshot.locals().get("1"); + assertNotNull(t1Locals); + assertEquals(77, t1Locals.get("locI")); + + // Deep immutability verification: mutating state after extraction does not alter snapshot + ds.setInt("x", 1000); + ds.setArrayElement("arr", 0, 999); + ds.setLocalInt(1, "locI", 1234); + assertEquals(99, snapshot.fields().get("x")); + assertArrayEquals(new int[]{1, 2, 3}, (int[]) snapshot.fields().get("arr")); + assertEquals(77, snapshot.locals().get("1").get("locI")); + + // Modifying input array after passing to snapshot constructor does not affect snapshot + int[] inputArr = new int[]{10, 20}; + StateSnapshot sManual = StateSnapshot.ofFields(Map.of("data", inputArr)); + inputArr[0] = 999; + assertArrayEquals(new int[]{10, 20}, (int[]) sManual.fields().get("data")); + } + + @Test + void extractPeterson_capturesFlagsAndTurn() { + PetersonState ps = PetersonState.of(new boolean[]{true, false, true}, 1); + ps.setFlag(1, true); + + StateSnapshot snapshot = StateSnapshotExtractor.extract(ps); + + assertArrayEquals(new boolean[]{true, true, true}, (boolean[]) snapshot.fields().get("flag")); + assertEquals(1, snapshot.fields().get("turn")); + assertEquals(-1, snapshot.fields().get("inCriticalSection")); + assertTrue(snapshot.locals().isEmpty()); + + // Immutability: modifying ps does not modify snapshot + ps.setFlag(0, false); + assertArrayEquals(new boolean[]{true, true, true}, (boolean[]) snapshot.fields().get("flag")); + } + + @Test + void extractCounter_capturesCounterAndRegisters() { + CounterState cs = CounterState.of(5, 2); + cs.setControl(true); + cs.setRegister(0, 10); + cs.setRegister(1, 20); + + StateSnapshot snapshot = StateSnapshotExtractor.extract(cs); + + assertEquals(5, snapshot.fields().get("counter")); + assertEquals(true, snapshot.fields().get("control")); + + assertEquals(10, snapshot.locals().get("0").get("register")); + assertEquals(20, snapshot.locals().get("1").get("register")); + } + + @Test + void extractPair_capturesHighLowAndObservation() { + PairState ps = PairState.of(10, 20, true); + ps.recordObservation(10, 19); + + StateSnapshot snapshot = StateSnapshotExtractor.extract(ps); + + assertEquals(10, snapshot.fields().get("high")); + assertEquals(20, snapshot.fields().get("low")); + assertEquals(true, snapshot.fields().get("control")); + assertEquals(10, snapshot.fields().get("observedHigh")); + assertEquals(19, snapshot.fields().get("observedLow")); + assertEquals(true, snapshot.fields().get("hasObservation")); + assertTrue(snapshot.locals().isEmpty()); + } + + @Test + void extractDeadlock_capturesFlagsAndControl() { + DeadlockState ds = DeadlockState.of(new boolean[]{true, false}); + ds.setControl(true); + + StateSnapshot snapshot = StateSnapshotExtractor.extract(ds); + + assertArrayEquals(new boolean[]{true, false}, (boolean[]) snapshot.fields().get("flag")); + assertEquals(true, snapshot.fields().get("control")); + assertTrue(snapshot.locals().isEmpty()); + } + + @Test + void extractDcl_capturesInstanceAndLockOwner() { + DclState ds = DclState.of(true); + ds.setInstance("myInstance"); + ds.setObservedInstance("myInstance"); + + StateSnapshot snapshot = StateSnapshotExtractor.extract(ds); + + assertEquals(true, snapshot.fields().get("initialized")); + assertEquals("myInstance", snapshot.fields().get("instance")); + assertEquals("myInstance", snapshot.fields().get("observedInstance")); + assertEquals(false, snapshot.fields().get("locked")); + assertEquals(-1, snapshot.fields().get("lockOwner")); + assertEquals(false, snapshot.fields().get("control")); + assertTrue(snapshot.locals().isEmpty()); + } + + @Test + void snapshotDeepCopy_handlesNullAndEmpty() { + StateSnapshot s1 = new StateSnapshot(null, null); + assertTrue(s1.fields().isEmpty()); + assertTrue(s1.locals().isEmpty()); + + StateSnapshot s2 = StateSnapshot.ofFields(Map.of("a", 1)); + assertEquals(1, s2.fields().get("a")); + assertTrue(s2.locals().isEmpty()); + } +} diff --git a/src/test/java/dev/samhb/interleave/search/TraceReplayerTest.java b/src/test/java/dev/samhb/interleave/search/TraceReplayerTest.java index f0ef946..d6e7f43 100644 --- a/src/test/java/dev/samhb/interleave/search/TraceReplayerTest.java +++ b/src/test/java/dev/samhb/interleave/search/TraceReplayerTest.java @@ -52,4 +52,45 @@ void replay_divergentOutcome_throwsCorruptedTraceException() { assertTrue(ex.getMessage().contains("recorded BLOCKED but execution produced ADVANCED")); } + + @Test + void captureSnapshots_recordsNPlusOneSnapshots() { + Program program = new Program(CounterState.of(0), List.of( + new ModelThread(0, List.of(new WriteCounterStep(0), new ReadCounterStep(0))) + )); + + Trace trace = Trace.of( + List.of(0, 0), + List.of(StepOutcome.ADVANCED, StepOutcome.ADVANCED), + TraceOutcome.COMPLETED + ); + + TraceReplayer replayer = new TraceReplayer(); + List snapshots = replayer.captureSnapshots(program, trace); + + assertEquals(3, snapshots.size(), "2-step trace must yield 3 snapshots (c0, c1, c2)"); + assertEquals(0, snapshots.get(0).fields().get("counter")); + assertEquals(1, snapshots.get(1).fields().get("counter")); + assertEquals(1, snapshots.get(2).fields().get("counter")); + assertEquals(1, snapshots.get(2).locals().get("0").get("register")); + } + + @Test + void enrich_attachesSnapshotsToTraceRecord() { + Program program = new Program(CounterState.of(0), List.of( + new ModelThread(0, List.of(new WriteCounterStep(0))) + )); + + dev.samhb.interleave.TraceRecord record = new dev.samhb.interleave.TraceRecord( + List.of(0), List.of(StepOutcome.ADVANCED), TraceOutcome.COMPLETED, "hash-test" + ); + + TraceReplayer replayer = new TraceReplayer(); + dev.samhb.interleave.TraceRecord enriched = replayer.enrich(program, record); + + assertEquals(2, enriched.states().size()); + assertEquals("hash-test", enriched.programHash()); + assertEquals(0, enriched.states().get(0).fields().get("counter")); + assertEquals(1, enriched.states().get(1).fields().get("counter")); + } } From 7f848b5bc3fc775f031d8b0bb9a649b3c31a78b6 Mon Sep 17 00:00:00 2001 From: Samuel Date: Mon, 12 Oct 2026 22:37:19 -0400 Subject: [PATCH 2/3] fix: address CodeRabbit review feedback on snapshots and runner - Add Javadoc to StateSnapshotExtractor and StateSnapshot private helpers. - Limit onTraceCreated replay to VIOLATION and DEADLOCK outcomes in InterleaveRunner. - Cap display length for array formatting in visualizer.js formatVal. Co-authored-by: Codex --- docs/visualizer.js | 2 +- .../samhb/interleave/InterleaveRunner.java | 3 +- .../samhb/interleave/core/StateSnapshot.java | 15 +++++++ .../core/StateSnapshotExtractor.java | 44 +++++++++++++++++++ 4 files changed, 62 insertions(+), 2 deletions(-) diff --git a/docs/visualizer.js b/docs/visualizer.js index b62dddc..b9563a2 100644 --- a/docs/visualizer.js +++ b/docs/visualizer.js @@ -118,7 +118,7 @@ function formatVal(v){ if(v === null) return 'null'; if(typeof v === 'boolean') return String(v); if(typeof v === 'number') return String(v); - if(Array.isArray(v)) return '[' + v.map(formatVal).join(', ') + ']'; + if(Array.isArray(v)) return capStr('[' + v.map(formatVal).join(', ') + ']'); if(typeof v === 'object') return capStr(JSON.stringify(v)); return capStr(String(v)); } diff --git a/src/main/java/dev/samhb/interleave/InterleaveRunner.java b/src/main/java/dev/samhb/interleave/InterleaveRunner.java index f96309e..ed0c673 100644 --- a/src/main/java/dev/samhb/interleave/InterleaveRunner.java +++ b/src/main/java/dev/samhb/interleave/InterleaveRunner.java @@ -198,7 +198,8 @@ public void onStateVisited(Configuration config) { @Override public void onTraceCreated(Trace trace) { TraceRecord record = trace.toRecord(); - if (program != null) { + if (program != null && (record.outcome() == TraceOutcome.VIOLATION + || record.outcome() == TraceOutcome.DEADLOCK)) { try { List states = new TraceReplayer().captureSnapshots(program, trace); record = record.withStates(states); diff --git a/src/main/java/dev/samhb/interleave/core/StateSnapshot.java b/src/main/java/dev/samhb/interleave/core/StateSnapshot.java index 1d2c295..4440d7f 100644 --- a/src/main/java/dev/samhb/interleave/core/StateSnapshot.java +++ b/src/main/java/dev/samhb/interleave/core/StateSnapshot.java @@ -28,6 +28,13 @@ public record StateSnapshot( locals = deepCopyLocals(locals); } + /** + * Performs a deep defensive copy of a field map, cloning primitive arrays (int[], boolean[]) + * and returning an unmodifiable map. Returns an empty map if the input is null or empty. + * + * @param map map of field names to values + * @return unmodifiable defensive copy with cloned arrays + */ private static Map deepCopyFields(Map map) { if (map == null || map.isEmpty()) { return Map.of(); @@ -45,6 +52,14 @@ private static Map deepCopyFields(Map map) { return Collections.unmodifiableMap(copy); } + /** + * Performs a deep defensive copy of a nested thread locals map, cloning any nested + * primitive arrays and returning an unmodifiable outer map. Returns an empty map if + * the input is null or empty. + * + * @param map map of thread id strings to local maps + * @return unmodifiable defensive copy of nested locals + */ private static Map> deepCopyLocals(Map> map) { if (map == null || map.isEmpty()) { return Map.of(); diff --git a/src/main/java/dev/samhb/interleave/core/StateSnapshotExtractor.java b/src/main/java/dev/samhb/interleave/core/StateSnapshotExtractor.java index 1a2475a..8f5956c 100644 --- a/src/main/java/dev/samhb/interleave/core/StateSnapshotExtractor.java +++ b/src/main/java/dev/samhb/interleave/core/StateSnapshotExtractor.java @@ -12,6 +12,9 @@ */ public final class StateSnapshotExtractor { + /** + * Non-instantiable utility class. + */ private StateSnapshotExtractor() {} /** @@ -38,6 +41,12 @@ public static StateSnapshot extract(SharedState state) { } } + /** + * Extracts fields and thread locals from a dynamic DSL state. + * + * @param ds the dynamic state + * @return snapshot with fields declared in ds and locals per thread + */ private static StateSnapshot extractDynamic(DynamicState ds) { Map fields = new LinkedHashMap<>(); for (FieldDecl f : ds.decl().fields()) { @@ -68,6 +77,13 @@ private static StateSnapshot extractDynamic(DynamicState ds) { return new StateSnapshot(fields, locals); } + /** + * Extracts fields from a Peterson state: {@code flag} boolean array, {@code turn} integer, + * and {@code inCriticalSection} count. + * + * @param ps the Peterson state + * @return snapshot with Peterson fields + */ private static StateSnapshot extractPeterson(PetersonState ps) { Map fields = new LinkedHashMap<>(); boolean[] flags = new boolean[ps.threadCount()]; @@ -80,6 +96,13 @@ private static StateSnapshot extractPeterson(PetersonState ps) { return StateSnapshot.ofFields(fields); } + /** + * Extracts fields ({@code counter}, {@code control}) and thread locals ({@code register}) + * from a counter state. + * + * @param cs the counter state + * @return snapshot with counter fields and per-thread register locals + */ private static StateSnapshot extractCounter(CounterState cs) { Map fields = new LinkedHashMap<>(); fields.put("counter", cs.counter()); @@ -92,6 +115,13 @@ private static StateSnapshot extractCounter(CounterState cs) { return new StateSnapshot(fields, locals); } + /** + * Extracts fields from a Pair state: {@code high}, {@code low}, {@code control}, + * {@code observedHigh}, {@code observedLow}, and {@code hasObservation}. + * + * @param ps the pair state + * @return snapshot with pair fields + */ private static StateSnapshot extractPair(PairState ps) { Map fields = new LinkedHashMap<>(); fields.put("high", ps.high()); @@ -103,6 +133,12 @@ private static StateSnapshot extractPair(PairState ps) { return StateSnapshot.ofFields(fields); } + /** + * Extracts fields from a Deadlock state: {@code flag} boolean array and {@code control} flag. + * + * @param ds the deadlock state + * @return snapshot with deadlock fields + */ private static StateSnapshot extractDeadlock(DeadlockState ds) { Map fields = new LinkedHashMap<>(); boolean[] flags = new boolean[ds.threadCount()]; @@ -114,6 +150,14 @@ private static StateSnapshot extractDeadlock(DeadlockState ds) { return StateSnapshot.ofFields(fields); } + /** + * Extracts fields from a double-checked locking state: {@code initialized}, {@code instance} + * (encoded as "null" string or string value), {@code locked}, {@code lockOwner}, + * {@code control}, and {@code observedInstance} (encoded as "null" string or string value). + * + * @param ds the DCL state + * @return snapshot with DCL fields + */ private static StateSnapshot extractDcl(DclState ds) { Map fields = new LinkedHashMap<>(); fields.put("initialized", ds.initialized()); From e4ed854d54994533b3a10f2ba44517d8bb5b4797 Mon Sep 17 00:00:00 2001 From: Samuel Date: Mon, 12 Oct 2026 22:55:57 -0400 Subject: [PATCH 3/3] fix: address PR review feedback on array exposure, deadlock traces, and e2e assertions Address CodeRabbit review threads on defensive array copying in snapshot accessors, deadlock trace snapshot enrichment in benchmark harness, specific value-cell assertions in Playwright e2e tests, and new state variable diff highlighting. Co-authored-by: Codex --- docs/visualizer-e2e.mjs | 24 +++++++++------ docs/visualizer.js | 4 +-- .../samhb/interleave/core/StateSnapshot.java | 20 +++++++++++++ .../interleave/report/BenchmarkHarness.java | 8 ++--- .../core/StateSnapshotExtractorTest.java | 30 +++++++++++++++++++ .../report/BenchmarkHarnessTest.java | 19 ++++++++++++ 6 files changed, 90 insertions(+), 15 deletions(-) diff --git a/docs/visualizer-e2e.mjs b/docs/visualizer-e2e.mjs index 4cb587f..d0599cf 100644 --- a/docs/visualizer-e2e.mjs +++ b/docs/visualizer-e2e.mjs @@ -131,9 +131,9 @@ async function runTests() { const config4Label = await page.locator('#selectedIdxLabel').textContent(); assert(config4Label.includes('config 4'), 'State strip header shows config 4'); - const stateCells = await page.locator('#stateStrip table tbody tr').allTextContents(); - const counterRow4 = stateCells.find((row) => row.includes('counter')); - assert(counterRow4 != null && counterRow4.includes('1'), 'State strip at config 4 displays counter = 1'); + const counterRow4 = page.locator('#stateStrip table tbody tr').filter({ hasText: 'counter' }); + const counterVal4 = await counterRow4.locator('td').nth(2).textContent(); + assert(counterVal4?.trim() === '1', 'State strip at config 4 displays counter = 1'); // ------------------------------------------------------------- // Test 3: Interactive Row Click & State Diff Highlighting @@ -147,16 +147,22 @@ async function runTests() { const config3Label = await page.locator('#selectedIdxLabel').textContent(); assert(config3Label.includes('config 3'), 'State strip header updates to config 3'); - // In config 3, counter changed from 0 to 1, so .val-changed should be present - const changedCellCount3 = await page.locator('#stateStrip .val-changed').count(); - assert(changedCellCount3 > 0, 'State strip contains highlighted .val-changed cells on value change'); + // In config 3, counter changed from 0 to 1, so counter value cell must have .val-changed + const counterRow3 = page.locator('#stateStrip table tbody tr').filter({ hasText: 'counter' }); + const isCounterChanged3 = await counterRow3.locator('td').nth(2).locator('.val-changed').count() > 0; + assert(isCounterChanged3, 'State strip at config 3 highlights counter value cell with .val-changed'); + + // Click config 4: no values changed from config 3, so .val-changed must be absent + await timelineRows.nth(4).click(); + const changedCellCount4 = await page.locator('#stateStrip .val-changed').count(); + assert(changedCellCount4 === 0, 'State strip at config 4 has 0 .val-changed cells when no values changed'); // Click config 0 (initial state: counter = 0) await timelineRows.nth(0).click(); assert(await timelineRows.nth(0).evaluate((el) => el.classList.contains('active-row')), 'Row 0 becomes active on click'); - const stateCells0 = await page.locator('#stateStrip table tbody tr').allTextContents(); - const counterRow0 = stateCells0.find((row) => row.includes('counter')); - assert(counterRow0 != null && counterRow0.includes('0'), 'State strip at config 0 displays counter = 0'); + const counterRow0 = page.locator('#stateStrip table tbody tr').filter({ hasText: 'counter' }); + const counterVal0 = await counterRow0.locator('td').nth(2).textContent(); + assert(counterVal0?.trim() === '0', 'State strip at config 0 displays counter = 0'); // ------------------------------------------------------------- // Test 4: Keyboard Navigation (Enter and Space) diff --git a/docs/visualizer.js b/docs/visualizer.js index b9563a2..d456e6b 100644 --- a/docs/visualizer.js +++ b/docs/visualizer.js @@ -500,7 +500,7 @@ function renderStateStrip(){ tdN.append(mut); } const prevVal = prevSnapshot?.fields ? prevSnapshot.fields[name] : undefined; - const isChanged = prevSnapshot != null && prevVal !== undefined && !isValEqual(prevVal, val); + const isChanged = prevSnapshot != null && !isValEqual(prevVal, val); const tdV = renderValCell(val, isChanged); tr.append(tdS, tdN, tdV); tbody.append(tr); @@ -533,7 +533,7 @@ function renderStateStrip(){ tdN.append(mut); } const prevVal = prevSnapshot?.locals?.[tid] ? prevSnapshot.locals[tid][name] : undefined; - const isChanged = prevSnapshot != null && prevVal !== undefined && !isValEqual(prevVal, val); + const isChanged = prevSnapshot != null && !isValEqual(prevVal, val); const tdV = renderValCell(val, isChanged); tr.append(tdS, tdN, tdV); tbody.append(tr); diff --git a/src/main/java/dev/samhb/interleave/core/StateSnapshot.java b/src/main/java/dev/samhb/interleave/core/StateSnapshot.java index 4440d7f..4a403d5 100644 --- a/src/main/java/dev/samhb/interleave/core/StateSnapshot.java +++ b/src/main/java/dev/samhb/interleave/core/StateSnapshot.java @@ -71,6 +71,26 @@ private static Map> deepCopyLocals(Map fields() { + return deepCopyFields(fields); + } + + /** + * Returns an unmodifiable defensive copy of the snapshot's locals with cloned array values. + * + * @return unmodifiable map of thread locals with array copies + */ + @Override + public Map> locals() { + return deepCopyLocals(locals); + } + /** * Factory for snapshots with fields only. * diff --git a/src/main/java/dev/samhb/interleave/report/BenchmarkHarness.java b/src/main/java/dev/samhb/interleave/report/BenchmarkHarness.java index bce8c1e..b39a9f7 100644 --- a/src/main/java/dev/samhb/interleave/report/BenchmarkHarness.java +++ b/src/main/java/dev/samhb/interleave/report/BenchmarkHarness.java @@ -308,11 +308,11 @@ private static boolean isFailure(DfsResult result) { * Combines exploration outcomes and measured store diagnostics into a benchmark row. * @param strategy exploration strategy used for these results * @param bugName benchmark program name + * @param program program whose steps were explored * @param result completed exploration result * @param verdict reported exploration verdict * @param failingTrace representative failure trace, or null when absent * @param storeType visited-store strategy represented by this row - * @param program program whose steps were explored * @param store visited-position store for this run * @param preemptionsUsed preemption bound used, or null for an unbounded strategy * @return benchmark row preserving verdict, trace, measurements, and store diagnostics @@ -413,14 +413,14 @@ private static String cbVerdict(DfsResult result, StoreType storeType) { } /** - * Finds the first failing trace in the result. + * Finds the first failing or deadlocked trace in the result. * * @param result the exploration result - * @return the first trace with VIOLATION outcome, or null if none + * @return the first trace with VIOLATION or DEADLOCK outcome, or null if none */ private static Trace findFailingTrace(DfsResult result) { return result.traces().stream() - .filter(t -> t.outcome() == TraceOutcome.VIOLATION) + .filter(t -> t.outcome() == TraceOutcome.VIOLATION || t.outcome() == TraceOutcome.DEADLOCK) .findFirst() .orElse(null); } diff --git a/src/test/java/dev/samhb/interleave/core/StateSnapshotExtractorTest.java b/src/test/java/dev/samhb/interleave/core/StateSnapshotExtractorTest.java index 14c70a6..b7e8fc2 100644 --- a/src/test/java/dev/samhb/interleave/core/StateSnapshotExtractorTest.java +++ b/src/test/java/dev/samhb/interleave/core/StateSnapshotExtractorTest.java @@ -150,4 +150,34 @@ void snapshotDeepCopy_handlesNullAndEmpty() { assertEquals(1, s2.fields().get("a")); assertTrue(s2.locals().isEmpty()); } + + @Test + void snapshotAccessors_returnDefensiveCopiesOfArrays() { + boolean[] flags = new boolean[]{false, false}; + int[] arr = new int[]{10, 20}; + Map fields = Map.of("flag", flags, "arr", arr); + Map> locals = Map.of("0", Map.of("localArr", new int[]{99})); + + StateSnapshot snapshot = new StateSnapshot(fields, locals); + + // Mutate array returned by fields() + boolean[] returnedFlags = (boolean[]) snapshot.fields().get("flag"); + returnedFlags[0] = true; + int[] returnedArr = (int[]) snapshot.fields().get("arr"); + returnedArr[0] = 999; + + // Mutate array returned by locals() + int[] returnedLocalArr = (int[]) snapshot.locals().get("0").get("localArr"); + returnedLocalArr[0] = -1; + + // Verify snapshot internal state is uncorrupted + boolean[] freshFlags = (boolean[]) snapshot.fields().get("flag"); + assertFalse(freshFlags[0], "Mutating returned flags must not mutate snapshot internal state"); + + int[] freshArr = (int[]) snapshot.fields().get("arr"); + assertEquals(10, freshArr[0], "Mutating returned int array must not mutate snapshot internal state"); + + int[] freshLocalArr = (int[]) snapshot.locals().get("0").get("localArr"); + assertEquals(99, freshLocalArr[0], "Mutating returned local array must not mutate snapshot internal state"); + } } diff --git a/src/test/java/dev/samhb/interleave/report/BenchmarkHarnessTest.java b/src/test/java/dev/samhb/interleave/report/BenchmarkHarnessTest.java index fa11a62..d45f7a2 100644 --- a/src/test/java/dev/samhb/interleave/report/BenchmarkHarnessTest.java +++ b/src/test/java/dev/samhb/interleave/report/BenchmarkHarnessTest.java @@ -167,4 +167,23 @@ void statesExploredTable_formatsCorrectly() { assertTrue(reduction.contains("STATIC_POR (exact): 50")); assertTrue(reduction.contains("DPOR (exact): 30")); } + + @Test + void runProgram_deadlockCapturesStateSnapshots() { + BenchmarkHarness harness = new BenchmarkHarness(); + BenchmarkProgram deadlockProg = BugCorpus.all().stream() + .filter(p -> "DEADLOCK".equals(p.expectedVerdict())) + .findFirst() + .orElseThrow(); + + List results = harness.runProgram(deadlockProg); + BenchmarkResult dfsDeadlock = results.stream() + .filter(r -> "DFS".equals(r.strategy()) && r.storeType() == StoreType.EXACT) + .findFirst() + .orElseThrow(); + + assertEquals("DEADLOCK", dfsDeadlock.verdict()); + assertTrue(dfsDeadlock.failingTrace().isPresent(), "Deadlock should have a failing/deadlocked trace"); + assertFalse(dfsDeadlock.states().isEmpty(), "Deadlock benchmark result should capture state snapshots"); + } }