1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
|
package main
// Job state: one execution of one command.
//
// A job runs asynchronously because solve times span five orders of magnitude
// -- 0.1s for a toy model, over two minutes for protocol-design/instance_19 --
// so nothing may block on one.
//
// Subscribers get a snapshot *and* a channel of subsequent states, handed out
// atomically, so a browser connecting mid-solve can neither miss the result nor
// see a torn view of it.
//
// The job state machine itself (parse, run, supersede, cancel) lives on
// *server in serve.go: there is exactly one model and one job in flight, so
// there is nothing left for a manager type to manage.
import (
"sync"
"time"
)
// JobState is the coarse phase of a job, as shown in the UI status line.
type JobState string
const (
StateParsing JobState = "parsing"
StateTranslating JobState = "translating"
StateSolving JobState = "solving"
StateDone JobState = "done"
StateError JobState = "error"
StateCancelled JobState = "cancelled"
)
// terminal reports whether no further updates will follow.
func (s JobState) terminal() bool {
return s == StateDone || s == StateError || s == StateCancelled
}
// Progress carries the solver statistics reported during translation/solving.
type Progress struct {
Solver string
Bitwidth int
PrimaryVars int
TotalVars int
Clauses int
}
// RunResult is the outcome of a satisfiable-or-not solve.
type RunResult struct {
Satisfiable bool
InstanceXML string
TraceLength int
LoopState int
DurationMs int64
}
// JobError is a failure with optional source position, so the UI can point at
// the offending line of the .als file.
type JobError struct {
Kind string
Message string
Filename string
Line int
Column int
}
func (e *JobError) Error() string { return e.Kind + ": " + e.Message }
// JobStatus is an immutable snapshot of a job.
//
// These types carry no json tags: only viewState is ever serialized, and it is
// built from a JobStatus rather than being one.
type JobStatus struct {
State JobState
Command int
Label string
Progress *Progress
Result *RunResult
Err *JobError
StartedAt time.Time
ElapsedMs int64
}
// job is the mutable state behind a JobStatus, plus its subscriber set.
type job struct {
mu sync.Mutex
status JobStatus
subs map[chan JobStatus]struct{}
// cancelled records that *we* killed the solver, so execute can tell a
// deliberate kill (cancel, or being superseded by a newer run) apart from
// the JVM dying on its own.
cancelled bool
}
func newJob(commandIndex int, label string) *job {
return &job{
status: JobStatus{
State: StateParsing,
Command: commandIndex,
Label: label,
StartedAt: time.Now(),
},
subs: make(map[chan JobStatus]struct{}),
}
}
// withElapsed fills in ElapsedMs for a still-running job. Terminal jobs keep
// the elapsed time they finished with.
func withElapsed(s JobStatus) JobStatus {
if !s.State.terminal() {
s.ElapsedMs = time.Since(s.StartedAt).Milliseconds()
}
return s
}
func (j *job) snapshot() JobStatus {
j.mu.Lock()
defer j.mu.Unlock()
return withElapsed(j.status)
}
// markCancelled records that we are about to kill this job's solver, and
// reports whether this call is the one that did so.
//
// The caller kills only when it gets true. A job stays non-terminal for a
// moment after its solver is killed -- its execute goroutine has to wake on the
// closed frame channel first -- so a second look at it would otherwise conclude
// it is still running and kill again, this time hitting whichever process has
// since taken the worker's place.
func (j *job) markCancelled() bool {
j.mu.Lock()
defer j.mu.Unlock()
if j.cancelled {
return false
}
j.cancelled = true
return true
}
func (j *job) wasCancelled() bool {
j.mu.Lock()
defer j.mu.Unlock()
return j.cancelled
}
// update mutates the job under lock and fans the new snapshot out to
// subscribers. On a terminal state it also closes and releases them.
func (j *job) update(f func(*JobStatus)) {
j.mu.Lock()
f(&j.status)
if j.status.State.terminal() && j.status.ElapsedMs == 0 {
j.status.ElapsedMs = time.Since(j.status.StartedAt).Milliseconds()
}
s := withElapsed(j.status)
terminal := s.State.terminal()
subs := make([]chan JobStatus, 0, len(j.subs))
for ch := range j.subs {
subs = append(subs, ch)
if terminal {
delete(j.subs, ch)
}
}
j.mu.Unlock()
for _, ch := range subs {
select {
case ch <- s:
default:
// Subscriber is not keeping up; it can re-read via snapshot().
}
if terminal {
close(ch)
}
}
}
// subscribe returns the current snapshot and a channel of subsequent updates.
// The channel is closed once a terminal state has been delivered, and is nil if
// the job has already finished.
//
// Both are produced under one lock so a job that finishes between the snapshot
// and the subscription cannot slip through unobserved.
func (j *job) subscribe() (JobStatus, chan JobStatus) {
j.mu.Lock()
defer j.mu.Unlock()
s := withElapsed(j.status)
if s.State.terminal() {
return s, nil
}
ch := make(chan JobStatus, 8)
j.subs[ch] = struct{}{}
return s, ch
}
// Subscribers do not need to unsubscribe: every job reaches a terminal state
// (done, error or cancelled -- a killed solver produces "cancelled" rather than
// silence), and update() closes and releases every channel when it does. A
// consumer therefore just ranges over the channel until it closes.
|