Documentation
¶
Overview ¶
Package deadlock provides a simple algorithm checker. It contains a DSL to describe multi-process system and a detector for deadlocks in the concurrent product of the processes.
Index ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
This section is empty.
Types ¶
type Detector ¶
Detector searches the state space of given system and reports presence of deadlocks.
func NewDetector ¶
func NewDetector() Detector
type LocationSet ¶
type Printer ¶
type Printer struct {
// contains filtered or unexported fields
}
Printer outputs reports in Graphviz's dot notation
func NewPrinter ¶
type Process ¶
type Process interface {
Id() ProcessId
EntryPoint() rule.Location
Rules() rule.RuleSet
HaltingPoints() []rule.Location
EnterAt(rule.Location) Process
Define(rule.Rule) Process
HaltAt(...rule.Location) Process
}
Process represents a single process in a concurrent system.
func NewProcess ¶
func NewProcess() Process
type Report ¶
type Report interface {
Visited() StateSet
Transited() TransitionSet
Initial() StateId
Accepting() StateSet
Deadlocked() StateSet
Traces() TransitionSet
}
Report contains the result of the state space searching
type State ¶
type State interface {
Id() StateId
Locations() LocationSet
Upstream() TransitionId
}
State represents a state of the system's each moment i.e. where processes are and what the value of variables are.
type System ¶
type System interface {
InitVars() vars.Shared
Processes() []Process
Declare(vars.Shared) System
Register(ProcessId, Process) System
}
System represents a set of processes. In the deadlock detection, they act concurrently accessing the pre-declared global shared variables.
type Transition ¶
type Transition interface {
Id() TransitionId
Process() ProcessId
Label() rule.Label
Source() StateId
Target() StateId
}
Transition represents a transition from the Source state to the Target state.
type TransitionId ¶
type TransitionId string
type TransitionSet ¶
type TransitionSet map[TransitionId]Transition
Directories
¶
| Path | Synopsis |
|---|---|
|
Package rule provides human-readable DSL to define transition rules.
|
Package rule provides human-readable DSL to define transition rules. |
|
do
Package do provides human-readable DSL for variable mutations.
|
Package do provides human-readable DSL for variable mutations. |
|
vars
Package vars provides variables shared by multiple processes.
|
Package vars provides variables shared by multiple processes. |
|
when
Package when provides human-readable DSL for conditional transitions.
|
Package when provides human-readable DSL for conditional transitions. |