summaryrefslogtreecommitdiff
path: root/agreement/state_machine_test.go
blob: 6946a051ec64816c230b8d83ad898d9c5b69c367 (plain)
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
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
// Copyright (C) 2019-2023 Algorand, Inc.
// This file is part of go-algorand
//
// go-algorand is free software: you can redistribute it and/or modify
// it under the terms of the GNU Affero General Public License as
// published by the Free Software Foundation, either version 3 of the
// License, or (at your option) any later version.
//
// go-algorand is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU Affero General Public License for more details.
//
// You should have received a copy of the GNU Affero General Public License
// along with go-algorand.  If not, see <https://www.gnu.org/licenses/>.

package agreement

import (
	"bytes"
	"fmt"
	"os"
	"strings"

	"github.com/algorand/go-algorand/logging"
)

const truncateIOTrace = false

/*
 * testable.go
 * -----------
 *
 * This file defines a number of interfaces that state machines can implement, so that they
 * are easier to unit test. In particular, implementing these interfaces:
 * - allows us to validate state machines against expected traces
 *
 * We generally model state machines as I/O automata, even though our machines are single-threaded
 * and synchronous. We can generate "traces", which
 * are sequences of input and output actions visible to the outside world. "Traces" do not
 * include state, or internal actions. We validate our state machines against sequences
 * of expected traces (which are actually glorified safety properties).
 * Traces are associated with safety properties, and liveness properties.
 * A trace is not a fragment; it is a history since the instatiation of the automata at its
 * start state.
 *
 * These traces are heavily related to state machine contracts, which are a stateful version
 * of safety property (and liveness property) verification.
 *
 * -----------Rationale for using the model-----------
 * 1. the model defines "parallel composition" of automata A and B.
 *    If A satisfies trace property P_A, and B satisfies trace property P_B, then A*B satisfies P_A*P_B
 *    (which are just the rules applied over the combined trace). This gives an immediate way
 *    to compose trace safety checking when we compose machines together (in particular, making
 *    sure we satisfy the parallel composition criteria: internal actions of A are disjoint with B,
 *    outputs of A and B are disjoint)
 * 2. The model also defines simulation relations: if there is a simulation relation from A to B, then
 *    traces(A) \subseteq \traces(B) (A is lower level, B is a higher level (more abstract) automaton.
 *    (A implements, or simualates, B)
 * 3. Instead of reasoning about inputs and outputs, and introducing an additional router
 *    assumption to pipe outputs back into inputs, we can abstract away the router and reason about the
 *    underlying state machine. This allows us to put post-conditions on event dispatches.
 *
 * -----------
 * Key Ideas:
 *   - test cases (specific traces) are safety properties
 *   - even though I/O automata are asynchronous, we still gain benefits from modeling our (synchronous) state
 *     machines this way. In particular, in the implementation, which is stricter than the model:
 *       - (a) only one action can be enabled at a time (I'm conflating events and actions)
 *       - (b) input events are always spaced out far enough to allow output actions to complete (demux'd)
 *       - (c) state machines can generate only a single action in response to an event
 *       - note that traditional Synchronous State machine models transition as a function of ALL incoming
 *         events. Algorand agreement only delivers one event at a time (due to router mux). This necessitates
 *         part (c) above.
 *       - In particular, this means that traces will look like; Out; In; Out; In; Out (if the mapping from
 *         listeners to IO automata are implemented correctly).
 */

// ioTrace is a collapsed execution trace generated by a state machine.
// It cannot contain nil events. It can handle dispatched event stacks that
// aren't immediately succeeded by an output event (wrapping internal actions)
// if we decide not to hide internal actions (fed through the router) and expose them
// when composing traces of compositions of state machines.
type ioTrace struct {
	events []event // input and output actions
}

func (t *ioTrace) length() int {
	return len(t.events)
}

func (t *ioTrace) extend(eventsToAppend ...event) error {
	if eventsToAppend == nil {
		return fmt.Errorf("Cannot extend trace with nil event")
	}
	t.events = append(t.events, eventsToAppend...)
	return nil
}

func (t *ioTrace) checkWellFormed() error {
	for i := 0; i < len(t.events); i++ {
		if t.events[i] == nil {
			return fmt.Errorf("Trace contains nil event")
		}
	}
	return nil
}

// Primarily for debug purposes
func (t *ioTrace) String() string {
	const TruncLen = 500
	var buf bytes.Buffer
	buf.WriteString("{\n")
	for i := 0; i < len(t.events); i++ {
		buf.WriteString(fmt.Sprintf("\t%v |", t.events[i].ComparableStr()))
		if i%2 == 0 {
			buf.WriteString("\n")
		}
	}
	buf.WriteString("}\n")

	if !truncateIOTrace {
		return buf.String()
	}

	l := buf.Len()
	g := l - TruncLen // try to truncate
	prepend := ""
	if g < 0 {
		g = 0
	} else {
		prepend = "(truncated...)\t"
	}
	return prepend + string(buf.Bytes()[g:])
}

// test helpers
func (t ioTrace) Contains(e event) bool {
	return t.ContainsFn(func(b event) bool {
		return e.ComparableStr() == b.ComparableStr()
	})
}

func (t ioTrace) ContainsString(s string) bool {
	return t.ContainsFn(func(b event) bool {
		return strings.Contains(b.ComparableStr(), s)
	})
}

func (t ioTrace) CountEvent(b event) (count int) {
	for _, e := range t.events {
		if e.ComparableStr() == b.ComparableStr() {
			count++
		}
	}
	return
}

// for each event, passes it into the given fn; if returns true, returns true.
func (t ioTrace) ContainsFn(compareFn func(b event) bool) bool {
	for _, ev := range t.events {
		if compareFn(ev) {
			return true
		}
	}
	return false
}

func (t ioTrace) countAction() (count int) {
	for _, ev := range t.events {
		if ev.t() == wrappedAction {
			count++
		}
	}
	return
}

// ioSafetyProp denotes whether some trace is "safe" according to itself
type ioSafetyProp interface {
	// returns bool whether trace is in the safety property. If false,
	// optionally accompanied by an informational message pertaining to why
	// the trace is not in the safety property. Err is set if we saw an
	// unforeseen error.
	containsTrace(trace ioTrace) (contains bool, info string, err error)

	// every safety prop also exposes the option to check it dynamically
	newPropChecker() ioPropChecker
}

// the safety prop that contains all traces (can be used as a stub)
type ioPropAll struct {
}

func (s ioPropAll) containsTrace(trace ioTrace) (bool, string, error) {
	return true, "", nil
}

func (s ioPropAll) newPropChecker() ioPropChecker {
	return new(ioPropAllChecker)
}

type ioPropAllChecker struct {
}

func (c ioPropAllChecker) addEvent(e event) error {
	return nil
}

// ioPropChecker is a stateful safety prop validator
type ioPropChecker interface {
	// add another event in order from the trace, returns error if the
	// addition of this event excludes the source trace from the safety prop
	addEvent(e event) error
}

type ioPropCheckerFactory interface {
	newPropChecker() ioPropChecker
}

// ioPropWrapper implements ioSafetyProp, wrapping an iopropChecker
type ioPropWrapper struct {
	ioPropCheckerFactory
}

func (w ioPropWrapper) containsTrace(trace ioTrace) (contains bool, info string, err error) {
	checker := w.newPropChecker()
	err = trace.checkWellFormed()
	if err != nil {
		return false, "", err
	}
	for _, e := range trace.events {
		valid := checker.addEvent(e)
		if valid != nil {
			return false, valid.Error(), nil
		}
	}
	return true, "", nil
}

// directMatchIoSafetyProp is a safety prop that returns "safe" if a trace
// contains the specified test trace as a prefix, or matches a prefix of the direct match
type directMatchIoSafetyProp struct {
	directMatchTrace ioTrace
}

// containsTrace validates traces if and only if they match our expected actions
func (e *directMatchIoSafetyProp) containsTrace(trace ioTrace) (bool, string, error) {
	for i := 0; i < trace.length(); i++ {
		if i >= e.directMatchTrace.length() {
			return true, "", nil
		}
		// compare using String(), in case event is uncomparable
		// This comparison is very loose, but we only need to match event types for now
		// Only exception: an error field type matches anything of same type
		if trace.events[i].ComparableStr() != e.directMatchTrace.events[i].ComparableStr() {
			return false, "", nil
		}
	}
	return true, "", nil
}

func (e *directMatchIoSafetyProp) newPropChecker() ioPropChecker {
	panic("Unsupported; direct match safety prop cannot dynamically check traces (yet)")
}

// ioAutomata is a traceable state machine. The trace hides internal actions.
// Why is this useful when listener is already checked? We can impose
// test-only safety properties, for instance. This is, in fact, how input/output
// unit test event matching works - it's expressed as a safety property.
// Eventually, checkedListener should implement ioAutomata! For now, we wrap
// checked listeners in ioAutomataConcrete to implement ioAutomata.
type ioAutomata interface {
	ioTraceable

	// #todo eventually, post refactor, these methods should be equivalent
	// to the listener interface. However, listener currently requires router
	// and player, which ioAutomata should fully encapsulate. Once we remove the
	// ioAutomata dependency on player (and wrap the router) the interfaces
	// can probably be combined.
	transition(input event) (err error, panicError error)
	transitionAll(inputs []event) (err error, panicError error)
}

type ioTraceable interface {
	// getTrace returns the trace of the execution so far.
	// note that it always starts at initialization, at the start state.
	getTrace() ioTrace
	// getTraceVisible returns a trace without hiding internal events.
	getTraceVisible() ioTrace
	// resetTrace resets the stored trace, erasing history, in effect
	// restarting it at the point when resetTrace is called
	resetTrace()
}

// ioAutomataConcrete is a concrete wrapper around listener, implementing ioAutomata.
// ioAutomataConcrete also implements router to help with assembling traces.
// Wraps listeners with a router and player object. Also catches panics and wraps them in an error.
type ioAutomataConcrete struct {
	listener

	// listeners need additional context. For now, we keep it static.
	routerCtx router // optional, set to router{} on default
	playerCtx player // optional, set to player{} by default

	// private
	savedHiddenTrace ioTrace // hides internal events, output of getTrace
	savedTrace       ioTrace
	rHandle          *routerHandle
}

func (w *ioAutomataConcrete) getTrace() ioTrace {
	return w.savedHiddenTrace
}

// resets the trace, for instance to make testing for recent events easier
func (w *ioAutomataConcrete) resetTrace() {
	w.savedHiddenTrace = ioTrace{}
	w.savedTrace = ioTrace{}
}

func (w *ioAutomataConcrete) getTraceVisible() ioTrace {
	return w.savedTrace
}

// Hijack router so that we can track internal events dispatched between state machines.
// Alternatively, we create a tracer interface and pass ourselves in
// as the tracer - but hijacking router seems to be less impactful since an interface
// already exists.
func (w *ioAutomataConcrete) dispatch(t *tracer, state player, e event, src stateMachineTag, dest stateMachineTag, r round, p period, s step) event {
	_ = w.savedTrace.extend(e)
	out := w.routerCtx.dispatch(t, state, e, src, dest, r, p, s)
	_ = w.savedTrace.extend(out)
	return out
}

func (w *ioAutomataConcrete) callHandler(inputTraceEvent event) (outEvent event, panicErr error) {
	logging.Base().SetOutput(nullWriter{})
	defer func() {
		logging.Base().SetOutput(os.Stderr)
		r := recover()
		if r != nil {
			panicErr = fmt.Errorf("%v", r)
		}
	}()
	if w.rHandle == nil {
		w.rHandle = &routerHandle{t: &tracer{log: serviceLogger{logging.Base()}}, r: w}
	}
	outEvent = w.listener.handle(*w.rHandle, w.playerCtx, inputTraceEvent)
	return
}

func (w *ioAutomataConcrete) transition(inputTraceEvent event) (err error, panicErr error) {
	out, callPanicErr := w.callHandler(inputTraceEvent)
	if callPanicErr != nil {
		// the first err will be more useful once state machines propagate errors upwards
		return err, callPanicErr
	}

	// extend saved traces
	err = w.savedHiddenTrace.extend(inputTraceEvent)
	if err != nil {
		return err, nil
	}
	err = w.savedHiddenTrace.extend(out)
	if err != nil {
		return err, nil
	}
	err = w.savedTrace.extend(inputTraceEvent)
	if err != nil {
		return err, nil
	}
	err = w.savedTrace.extend(out)
	if err != nil {
		return err, nil
	}

	return nil, nil
}

func (w *ioAutomataConcrete) transitionAll(inputs []event) (error, error) {
	for i := 0; i < len(inputs); i++ {
		err, panicErr := w.transition(inputs[i]) // a nil event is interpreted as no input
		if err != nil || panicErr != nil {
			return err, panicErr
		}
	}
	return nil, nil
}

/* Testing Utils */

type blackhole struct{}

func (blackhole) Write(data []byte) (int, error) {
	return len(data), nil
}

// deterministicTraceTestCase encapsulates a traditional unit test test case.
type determisticTraceTestCase struct {
	inputs          []event
	expectedOutputs []event
	safetyProps     []ioSafetyProp
}

// Validate takes a given automata at zero state, drives it with the test case input,
// and validates the output.
func (testCase *determisticTraceTestCase) Validate(automaton ioAutomata) (invalidErr error, runtimeErr error) {
	return testCase.ValidateAsExtension(automaton)
}

// ValidateAsExtension takes a given automata that is already in some state, drives it
// with some addition input (an "extension"), and validates the output.
func (testCase *determisticTraceTestCase) ValidateAsExtension(automaton ioAutomata) (invalidErr error, runtimeErr error) {
	// suppress error logging from contract-checkers
	logging.Base().SetOutput(blackhole{})
	defer func() {
		logging.Base().SetOutput(os.Stderr)
	}()

	if len(testCase.inputs) != len(testCase.expectedOutputs) && len(testCase.inputs) != len(testCase.expectedOutputs)+1 {
		return nil, fmt.Errorf("Malformed test case: either inputs and outputs must be same length, or inputs should be one longer than outputs")
	}

	// the automata may have already run some and generated a trace
	existingTraceLength := len(automaton.getTrace().events)

	// construct partial input and final expected extension traces
	allEvents := make([]event, len(testCase.expectedOutputs)*2)
	for i := 0; i < len(testCase.inputs); i++ {
		if i < len(testCase.expectedOutputs) {
			allEvents[2*i] = testCase.inputs[i]
			allEvents[2*i+1] = testCase.expectedOutputs[i]
		}
	}
	expectedFinalTrace := ioTrace{allEvents}
	err := expectedFinalTrace.checkWellFormed()
	if err != nil {
		return nil, fmt.Errorf("Outputs cannot contain nil events; %v", err)
	}
	err, panicErr := automaton.transitionAll(testCase.inputs)
	if err != nil {
		return nil, err
	}
	outputTrace := automaton.getTrace()
	outputTraceLen := outputTrace.length()
	outputTraceExtension := ioTrace{outputTrace.events[existingTraceLength:]}
	validator := directMatchIoSafetyProp{expectedFinalTrace}
	traceValid, _, runtimeErr := validator.containsTrace(outputTraceExtension)
	if runtimeErr != nil {
		return nil, runtimeErr
	}

	// any trace should be valid up to the point of panicking
	if !traceValid {
		invalidErr = errIOTraceDiverge{expected: expectedFinalTrace.String(), actual: outputTraceExtension.String()}
		return invalidErr, nil
	}

	if len(testCase.inputs) == len(testCase.expectedOutputs) {
		// we have one output for each input if and only if we did not ever panic
		if panicErr != nil {
			invalidErr = fmt.Errorf("Panicked when we were not expecting it: %v", panicErr)
			return invalidErr, nil
		}
	} else if len(testCase.inputs) == len(testCase.expectedOutputs)+1 {
		// we have a dangling final output if and only if we panicked
		if panicErr == nil {
			invalidErr = fmt.Errorf("Did not panic when we were expecting to")
			return invalidErr, nil
		}
	} else {
		invalidErr = fmt.Errorf("Input size (%v) is inconsistent with output size (%v)", testCase.inputs, testCase.expectedOutputs)
		return invalidErr, nil
	}

	if outputTraceLen < expectedFinalTrace.length() {
		if panicErr != nil {
			invalidErr = fmt.Errorf("Panicked early: %d:%d:\t%v",
				outputTraceLen, expectedFinalTrace.length(), panicErr)
			return invalidErr, nil
		}
		// since we are validating a synchronous state machine, the output trace should be as long as expected
		invalidErr = fmt.Errorf("Trace too short (%d:%d). %v %v",
			outputTraceLen, expectedFinalTrace.length(), expectedFinalTrace, outputTraceExtension)
		return invalidErr, nil
	}

	// finally, validate (the entire) output trace (not just the extension) against specified safety properties, if any
	for _, sp := range testCase.safetyProps {
		good, msg, err := sp.containsTrace(outputTrace)
		if err != nil {
			return nil, fmt.Errorf("Error evaluating safety property %v", sp)
		}
		if !good {
			return fmt.Errorf("Trace not in safety property: %v, %s", sp, msg), nil
		}
	}

	return nil, nil
}

// a convenience helper
type testCaseBuilder struct {
	inputs          []event
	expectedOutputs []event
	safetyProps     []ioSafetyProp
}

func (b *testCaseBuilder) Build() *determisticTraceTestCase {
	return &determisticTraceTestCase{b.inputs, b.expectedOutputs, b.safetyProps}
}

func (b *testCaseBuilder) AddInOutPair(input event, output event) {
	if b.inputs == nil {
		b.inputs = make([]event, 0, 1)
	}
	if b.expectedOutputs == nil {
		b.expectedOutputs = make([]event, 0, 1)
	}
	b.inputs = append(b.inputs, input)
	b.expectedOutputs = append(b.expectedOutputs, output)
}

func (b *testCaseBuilder) AddSafetyProp(prop ioSafetyProp) {
	if b.safetyProps == nil {
		b.safetyProps = make([]ioSafetyProp, 0, 1)
	}
	b.safetyProps = append(b.safetyProps, prop)
}

type errIOTraceDiverge struct {
	expected string
	actual   string
}

func (err errIOTraceDiverge) Error() string {
	return fmt.Sprintf("Expected: %s, Actual %s", err.expected, err.actual)
}

/* Utils for player testing */

// wrap actions as events so we can test player as a listener
func ev(a action) event {
	return wrappedActionEvent{a}
}

type wrappedActionEvent struct {
	action
}

func (e wrappedActionEvent) t() eventType {
	return wrappedAction
}

func (e wrappedActionEvent) String() string {
	return e.action.String()
}

func (e wrappedActionEvent) ComparableStr() string {
	return e.action.ComparableStr()
}

// ioAutomataConcretePlayer is a concrete wrapper around root router, implementing ioAutomata.
type ioAutomataConcretePlayer struct {
	*rootRouter

	savedTrace *ioTrace

	// need to stub out these objects
	t *tracer
}

func (w *ioAutomataConcretePlayer) getTrace() ioTrace {
	return *w.savedTrace
}

// resets the trace, for instance to make testing for recent events easier
func (w *ioAutomataConcretePlayer) resetTrace() {
	w.savedTrace = nil
}

func (w *ioAutomataConcretePlayer) getTraceVisible() ioTrace {
	panic("unsupported")
}

func (w *ioAutomataConcretePlayer) underlying() *player {
	return w.rootRouter.root.underlying().(*player)
}

func (w *ioAutomataConcretePlayer) callSubmitTop(inputTraceEvent event) (outEvents []event, panicErr error) {
	logging.Base().SetOutput(nullWriter{})
	defer func() {
		logging.Base().SetOutput(os.Stderr)
		r := recover()
		if r != nil {
			panicErr = fmt.Errorf("Panic: %v", r)
		}
	}()
	_, actions := w.rootRouter.submitTop(w.t, *w.underlying(), inputTraceEvent)
	// wrap all actions as events
	outEvents = make([]event, len(actions))
	for i, a := range actions {
		outEvents[i] = ev(a)
	}
	return
}

func (w *ioAutomataConcretePlayer) transition(inputTraceEvent event) (err error, panicErr error) {
	if w.savedTrace == nil {
		w.savedTrace = &ioTrace{}
	}
	if w.t == nil {
		w.t = &tracer{log: serviceLogger{logging.Base()}}
	}
	outEvents, callPanicErr := w.callSubmitTop(inputTraceEvent)
	if callPanicErr != nil {
		// the first err will be more useful once state machines propagate errors upwards
		return err, callPanicErr
	}

	// extend saved trace
	err = w.savedTrace.extend(inputTraceEvent)
	if err != nil {
		return err, nil
	}
	err = w.savedTrace.extend(outEvents...)
	if err != nil {
		return err, nil
	}

	return nil, nil
}

func (w *ioAutomataConcretePlayer) transitionAll(inputs []event) (error, error) {
	for i := 0; i < len(inputs); i++ {
		err, panicErr := w.transition(inputs[i]) // a nil event is interpreted as no input
		if err != nil || panicErr != nil {
			return err, panicErr
		}
	}
	return nil, nil
}