Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Hotfix for high memory usage #1465

Merged
merged 4 commits into from
Jul 26, 2024
Merged

Hotfix for high memory usage #1465

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
fd48556
Store only the requested amount of traces
bugarela Jul 24, 2024
9a63dde
Add CHANGELOG entry
bugarela Jul 24, 2024
4fecf3f
Remove unused import
bugarela Jul 24, 2024
8b787a9
Merge branch 'main' into gabriela/fix-memory-issue
bugarela Jul 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
### Deprecated
### Removed
### Fixed

- Fixed an issue that caused high memory usage on exploration (#1465)

### Security

## v0.21.0 -- 2024-06-16
Expand Down
4 changes: 2 additions & 2 deletions quint/src/runtime/testing.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,7 @@ export function compileAndTest(
recorder.onRunReturn(toMaybe(result), [])
}

const bestTrace = recorder.getBestTraces(1)[0].frame
const bestTrace = recorder.bestTraces[0].frame
// evaluate the result
if (result.isLeft()) {
// if the test failed, return immediately
Expand Down Expand Up @@ -210,7 +210,7 @@ export function compileAndTest(
}

// the test was run maxSamples times, and no errors were found
const bestTrace = recorder.getBestTraces(1)[0].frame
const bestTrace = recorder.bestTraces[0].frame
saveTrace(bestTrace, index, name, 'passed')
return {
name,
Expand Down
41 changes: 22 additions & 19 deletions quint/src/runtime/trace.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,6 @@ import { EvalResult } from './runtime'
import { verbosity } from './../verbosity'
import { Rng } from './../rng'
import { rv } from './impl/runtimeValue'
import { take } from 'lodash'

/**
* A snapshot of how a single operator (e.g., an action) was executed.
Expand Down Expand Up @@ -174,25 +173,25 @@ export interface TraceRecorder extends ExecutionListener {
clear: () => void

/**
* Get the best recorded traces.
* @param n the number of traces to get
* @returns the best recorded traces.
* The best recorded traces.
*/
getBestTraces(n: number): Trace[]
bestTraces: Trace[]
}

// a trace recording listener
export const newTraceRecorder = (verbosityLevel: number, rng: Rng): TraceRecorder => {
return new TraceRecorderImpl(verbosityLevel, rng)
export const newTraceRecorder = (verbosityLevel: number, rng: Rng, tracesToRecord: number = 1): TraceRecorder => {
return new TraceRecorderImpl(verbosityLevel, rng, tracesToRecord)
}

// a private implementation of a trace recorder
class TraceRecorderImpl implements TraceRecorder {
verbosityLevel: number
rng: Rng
currentFrame: ExecutionFrame
// all trace are stored here with their respective seeds
private traces: Trace[]
// how many traces to store
private tracesToStore: number
// best traces are stored here with their respective seeds
bestTraces: Trace[]
// whenever a run is entered, we store its seed here
private runSeed: bigint
// During simulation, a trace is built here.
Expand All @@ -202,27 +201,24 @@ class TraceRecorderImpl implements TraceRecorder {
// a tree of calls.
private frameStack: ExecutionFrame[]

constructor(verbosityLevel: number, rng: Rng) {
constructor(verbosityLevel: number, rng: Rng, tracesToStore: number) {
this.verbosityLevel = verbosityLevel
this.rng = rng
const bottom = this.newBottomFrame()
this.traces = []
this.tracesToStore = tracesToStore
this.bestTraces = []
this.runSeed = this.rng.getState()
this.currentFrame = bottom
this.frameStack = [bottom]
}

clear() {
this.traces = []
this.bestTraces = []
const bottom = this.newBottomFrame()
this.currentFrame = bottom
this.frameStack = [bottom]
}

getBestTraces(n: number): Trace[] {
return take(this.tracesByQuality(), n)
}

onUserOperatorCall(app: QuintApp) {
// For now, we cannot tell apart actions from other user definitions.
// https://github.com/informalsystems/quint/issues/747
Expand Down Expand Up @@ -331,10 +327,17 @@ class TraceRecorderImpl implements TraceRecorder {
traceToSave.result = outcome
traceToSave.args = trace

this.traces.push({ frame: traceToSave, seed: this.runSeed })
const traceWithSeed = { frame: traceToSave, seed: this.runSeed }

this.bestTraces.push(traceWithSeed)
this.sortTracesByQuality()
// Remove the worst trace (if there more traces than needed)
if (this.bestTraces.length > this.tracesToStore) {
this.bestTraces.pop()
}
Comment on lines +332 to +337
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This PR has been merged already. However, here is my concern. Now best traces are sorted on every run, even though only one new trace is added on every run. I don't know how large this.tracesToStore would be, but assuming it is n, we would have something like O(n * log(n)) operations spent on sorting in every run. Instead, you could just do one step of insertion sort, assuming that this.bestTraces is sorted already. This would give us a simple loop of n/2 iterations on average.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, I'm aware. But as I tried explaining in the description, n=1 in all existing use cases. It is only greater than 1 if you use the new CLI param --n-traces.

I did look up insertion sort implementations in typescript to use here, but there was nothing very handy and I just wanted to fix the memory issue. This seems like a fun thing to improve and benchmark tho, and my students will need to use this --n-traces features by the end of the semester, so I'll take care of performance eventually 😬

Copy link
Contributor

@konnov konnov Jul 29, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I mean, you don't need any special implementation for insertion sorting. To insert a new element e, you just do one iteration over the array x and find the index i such that x[i] <= e <= x[i+1] (of course, you have to take care of the cases i == 0 and i == x.length - 1). Then, you insert e at the position i. I guess, JS splice should be able to do that.

}

private tracesByQuality(): Trace[] {
private sortTracesByQuality() {
const fromResult = (r: Maybe<EvalResult>) => {
if (r.isNone()) {
return true
Expand All @@ -344,7 +347,7 @@ class TraceRecorderImpl implements TraceRecorder {
}
}

return this.traces.sort((a, b) => {
this.bestTraces.sort((a, b) => {
// Prefer short traces for error, and longer traces for non error.
// Therefore, trace a is better than trace b iff
// - when a has an error: a is shorter or b has no error;
Expand Down
4 changes: 2 additions & 2 deletions quint/src/simulation.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,7 @@ export function compileAndRun(
const newMainModuleCode = code.slice(mainStart, mainEnd - 1) + '\n' + extraDefs.join('\n')
const codeWithExtraDefs = code.slice(0, mainStart) + newMainModuleCode + code.slice(mainEnd)

const recorder = newTraceRecorder(options.verbosity, options.rng)
const recorder = newTraceRecorder(options.verbosity, options.rng, options.numberOfTraces)
const ctx = compileFromCode(
idGen,
codeWithExtraDefs,
Expand All @@ -134,7 +134,7 @@ export function compileAndRun(
res.value.eval()
}

const topTraces: Trace[] = recorder.getBestTraces(options.numberOfTraces)
const topTraces: Trace[] = recorder.bestTraces
const vars = evaluationState.vars.map(v => v.name)

topTraces.forEach((trace, index) => {
Expand Down
Loading