Documentation
¶
Overview ¶
Package tlc runs TLC over the declared cases of tla/CASES.tsv and reads what it says.
WHAT IT OWNS. Finding the TLC jar and the java that runs it (jar.go); the command line of one TLC run and its bounded execution (run.go); the reading of TLC's exit status and output into pass or fail, the statistics and the violated invariant, action or temporal property (outcome.go); the case plan tla/CASES.tsv into the cases a run is judged by, and its refusals (plan.go); the plan's checks against the tree and the choice of a run's cases (cases.go); the run records tla/RUNS.tsv (records.go); the inputs a case reads and the fingerprint a record names (inputs.go, with the runner's own files in fingerprint.go); and the suite that runs a selection of cases under one budget and writes the records (suite.go).
WHAT IT NEVER DOES. It downloads nothing, runs no more than two TLC workers per case, and never runs TLC beside the sources: every run happens in a private copy of the models under the output directory, because TLC writes an error-trace module and its binary beside the spec it was given, and a checkout that grew those files would no longer be the inputs a record names.
WHAT A FINGERPRINT COVERS. One case's inputs and nothing else: its configuration, its module and the modules that one extends or instantiates, its own row of the plan, and the runner's result files (the ones that decide how a result is produced and read, and how a plan row is read into the case a run is judged by; see fingerprint.go). Editing one model leaves the records of the cases that do not read it as they are.
WHY THE SOURCES ARE EMBEDDED. The runner's result files are part of every fingerprint (a change to how a result is read invalidates records that depend on that reading), and a binary built on one machine and run on a bench has no checkout of them. The binary therefore carries the bytes it was built from; internal/ci recomputes the fingerprint from the checkout's files, so a binary built from other files than the ones committed writes records that the class test refuses.
Index ¶
- Constants
- Variables
- func Accepts(c Case, code int, output, config string) bool
- func Carry(src Source, cases []Case, base []Record, runs ...[]Record) (kept []Record, dropped []Dropped, err error)
- func CasesRowPath(config string) string
- func CheckLimits(budget time.Duration, workers int, manual bool) error
- func CheckRunner(root string) error
- func CheckedFiles() []string
- func CopyModels(src, dst string) error
- func Digest(inputs []Input) string
- func Execute(ctx context.Context, r Run, log string) int
- func FindHelper(name, override string, lookPath func(string) (string, error)) (string, error)
- func JavaVersion(output string) (string, error)
- func ModuleReferences(text []byte) []string
- func OneJar(cases []Case, records []Record) error
- func Platform(goos, goarch string) (string, error)
- func ReadJavaVersion(ctx context.Context, java string) (string, error)
- func RequiredGroups(cases []Case) []string
- func RunnerFiles() (map[string][]byte, error)
- func StaleGroups(src Source, cases []Case, records []Record) ([]string, error)
- func ValidPlatform(label string) bool
- func WriteRecords(w io.Writer, records []Record) error
- type Case
- type Dropped
- type Executor
- type Input
- type Jar
- type MissingError
- type Options
- type Outcome
- type Record
- type Result
- type Run
- type Selection
- type Source
- type Violation
Constants ¶
const ( ExitPass = 0 // no error found ExitInvariant = 12 // an invariant (or a deadlock or assertion) is violated ExitProperty = 13 // an action or temporal property is violated ExitTimeout = 124 ExitNoStart = 127 // java could not be started )
TLC's exit statuses this package acts on. Any other status is a failure of the run, never a result.
const ( CasesFile = "CASES.tsv" RunsFile = "RUNS.tsv" )
CasesFile and RunsFile are the case plan and the run records, under tla/.
const ( DroppedStale = "stale" // its case reads other inputs than it was measured on DroppedGone = "not-in-the-plan" // the plan no longer declares its case )
The reasons a kept record is dropped.
const ( BoundedCap = 110 * time.Second ManualCap = 3600 * time.Second )
Bounds of a run. A bounded run is the only kind a required case can be measured by; a manual run is an explicit bench experiment and CI refuses it.
const JarEnv = "TLC_JAR"
JarEnv is the environment variable that names the TLC jar when --jar is not given. The Makefile target and the workflow set it; nothing else is looked at.
const RunnerDir = "pkg/tlc"
RunnerDir is where the runner's files live in a checkout, and the prefix their paths carry in the fingerprint.
Variables ¶
var BookkeepingFiles = []string{"cases.go", "doc.go", "fingerprint.go", "inputs.go", "jar.go", "records.go"}
BookkeepingFiles are the runner's other non-test files: the description (doc.go), the plan's checks against the tree and the choice of a run's cases (cases.go), the records (records.go), the jar and helper lookup (jar.go), the listing of a case's inputs and the list of TLC's standard modules (inputs.go) and this file. They decide no result, so a change to one of them stales no record. Every non-test file of the package is in exactly one of ResultFiles and BookkeepingFiles, so a new file cannot be left unclassified: TestEveryRunnerFileIsClassified.
var InputListFiles = []string{"inputs.go"}
InputListFiles are the bookkeeping files that decide which files a case's fingerprint covers (the parser of module references and the list of TLC's standard modules: inputs.go). They are in no fingerprint, because the digest is a function of the list they compute; but a binary built from another version of them computes another list than the checkout, so CheckRunner holds them to the checkout beside ResultFiles. They are also in BookkeepingFiles.
var LookPath = exec.LookPath
LookPath is exec.LookPath, named so callers pass one seam.
var Platforms = []string{
"linux-386", "linux-amd64", "linux-arm", "linux-arm64", "linux-loong64", "linux-mips", "linux-mips64",
"linux-mips64le", "linux-mipsle", "linux-ppc64", "linux-ppc64le", "linux-riscv64", "linux-s390x",
}
Platforms are the platform labels a record's host column may hold: the <goos>-<goarch> pairs of the operating systems the runner accepts (Linux only: TLC runs on a Linux bench) over the architectures Go supports there. The column never holds a machine's name.
var RecordsHeader = []string{"config", "module", "input_sha256", "input_files", "jar_sha256", "java_version", "host", "cpus", "started_utc", "workers", "generated", "distinct", "seconds", "exit", "result", "expected", "property", "budget", "mode"}
RecordsHeader is the header of tla/RUNS.tsv.
var ResultFiles = []string{"outcome.go", "plan.go", "run.go", "suite.go"}
ResultFiles are the runner's files that are inputs of every fingerprint, by name in RunnerDir.
Functions ¶
func Accepts ¶
Accepts reports whether the exit status and output are the result a case declares. It never accepts a timeout, a parse failure or a violation of some other property.
- pass: exit 0 and the completion line.
- invariant: exit 12 and one of the "|"-separated names is violated.
- action: exit 13 and one of the names is violated.
- temporal: exit 13 and a temporal violation, where the case's config selects exactly the one property the case names. TLC that names the violated property must name that one; TLC that does not is trusted on the config alone. config is the text of the case's .cfg file.
func Carry ¶
func Carry(src Source, cases []Case, base []Record, runs ...[]Record) (kept []Record, dropped []Dropped, err error)
Carry returns the records of base that a merge keeps beside the records of runs: those of declared cases that no run measured again and that are still current. A base record that is stale, or whose case the plan no longer declares, is left out and returned as dropped, so the merge can name it instead of carrying a measurement of other inputs.
func CasesRowPath ¶
CasesRowPath is the Path of a case's row of the plan.
func CheckLimits ¶
CheckLimits refuses a budget or worker count outside what a run may use: at most two TLC workers, and a budget that is positive and within the cap of its mode.
func CheckRunner ¶
CheckRunner holds the result files and the input-list files this binary was built from to the ones under root: a binary built from another checkout computes fingerprints or input lists that the checkout does not, so its verdict on what is stale is wrong. It returns an error naming the files that differ. A root that holds no pkg/tlc has no runner to compare (a bench copy of tla/ only), and nothing is checked.
func CheckedFiles ¶
func CheckedFiles() []string
CheckedFiles are the files CheckRunner holds to the checkout: ResultFiles and InputListFiles.
func CopyModels ¶
CopyModels copies the TLA+ modules and configurations of src into dst, replacing dst. TLC writes files beside the spec it is given (an error trace as a module and a binary), so a run never gets the checkout's own directory.
func Digest ¶
Digest is the fingerprint of a list of inputs: SHA-256 over, for each input in path order, its path, a NUL, the hex digest of its bytes and a newline. It holds no time, no host and no absolute path, so the same inputs give the same digest wherever they are read.
func Execute ¶
Execute is the Executor that runs java. The output goes to the log file, one stream for both of TLC's, and the run ends when the context does: a run that outlives its budget is killed and reported as ExitTimeout, never as a result.
func FindHelper ¶
FindHelper resolves an external program: the override when it is not empty (it must exist), otherwise the name on PATH. The path found is returned so a caller can echo it. lookPath is exec.LookPath in production.
The path is returned absolute. The program is started with another working directory than the caller's (a private copy of the models), so a path that is relative to the caller would name nothing there.
func JavaVersion ¶
JavaVersion reads the version out of what `java -version` prints (it goes to standard error): the quoted token of the first line that starts with `openjdk version "` or `java version "`, for example 21.0.12.1. Lines before it are skipped, so a "Picked up JAVA_TOOL_OPTIONS" line never gives the version. It is an error when no line is one, so a record never names a java of no version.
func ModuleReferences ¶
ModuleReferences returns the names of the modules a module's text extends or instantiates (`EXTENDS A, B`, `INSTANCE M`, `LOCAL INSTANCE M`, `F(x) == INSTANCE M WITH ...`), each once, in order of appearance, at every depth of nesting: a module may hold modules (`---- MODULE X ----` opens one and a line of `=` signs closes it), and each of them names modules of its own. A header may be split over two lines (`---- MODULE Inner` and the closing dashes on the next), and what follows a header or an inner module's closing line on its own line is read. A name that a module of the same text declares is not a file and is left out. Comments and strings are not read, neither is text before the first module header, nor anything after the line that closes the outermost module. A text with no module header is read up to its first closing line.
func OneJar ¶
OneJar refuses a set of records that was not all measured with one jar: a file mixing jars says nothing about any one of them. The refusal names each jar with how many records it measured, and the groups of the cases recorded under the jars other than the commonest, which are the ones to run again.
func Platform ¶
Platform is the label of the machine that runs TLC: goos and goarch as Go names them, joined by a dash. It refuses a pair that is not in Platforms.
func ReadJavaVersion ¶
ReadJavaVersion runs `java -version`, bounded by ctx, and returns its version. It runs java, so it belongs on a bench.
func RequiredGroups ¶
RequiredGroups returns the groups that hold a required case, sorted: the matrix a CI run derives.
func RunnerFiles ¶
RunnerFiles returns the runner's result files as they were when this binary was built, by their path under the checkout root.
func StaleGroups ¶
StaleGroups returns the groups, sorted, that hold a declared case with no current record among records: the groups to run again after an edit. A case is current when its record names the fingerprint src gives it now.
func ValidPlatform ¶
ValidPlatform reports whether label is in Platforms.
Types ¶
type Case ¶
type Case struct {
Config string // MCFoo.cfg
Module string // MCFoo.tla
Expected string // pass, invariant, action or temporal
Property string // "-" for pass; the violated name (or names joined by "|") otherwise
Deadlock string // check, or ignore-terminal (the models end in a terminal stutter by design)
Group string // the execution group; one CI job runs one group
Gate string // required, or bench
Debt string // "-", or why a bench case has no passing measurement
}
Case is one row of tla/CASES.tsv: one MC configuration, the module it instantiates and the result it must reach.
func LoadCases ¶
LoadCases reads tla/CASES.tsv under root and checks it against the tree: it must name every MC*.cfg exactly once and every module must exist.
func ParseCases ¶
ParseCases reads and checks the case plan. It does not look at the filesystem: LoadCases adds the checks against the files.
func Select ¶
Select returns the cases one run covers: a group, or shard number shard of shards (every shards'th case from shard) of the whole plan or, with a group, of that group's cases. A group's shards of its own size are its cases one at a time: run --bench measures a group so, a load trough before each case.
type Dropped ¶
type Dropped struct {
Config string
Group string // the case's group, "" when the plan no longer declares the case
Why string // DroppedStale or DroppedGone
}
Dropped is a record of the file a merge keeps that the merge does not carry, and why.
type Executor ¶
Executor runs TLC and leaves its combined output in the log file. It returns the exit status: ExitTimeout when the context ended first, ExitNoStart when the program could not be started. Its note is text already written to the log. Suites take an Executor so their bookkeeping is testable without java.
type Input ¶
Input is one thing a TLC run of a case reads: a file under tla/, the case's own row of the plan, or one of the runner's files. Path names it the way the fingerprint does (tla/<file>, tla/CASES.tsv#<config>, pkg/tlc/<file>), and SHA256 is the hex digest of its bytes.
type Jar ¶
type Jar struct {
Path string // absolute
Source string // "flag" or "env:TLC_JAR"
SHA256 string // hex
}
Jar is the TLC jar a run uses, and where its path came from.
func FindJar ¶
FindJar resolves the jar: the flag when it is not empty, otherwise the environment variable. There is no default location and nothing is downloaded. The jar must be a regular file; its digest is read now so every record of a run names the same jar even when the file is replaced while the run goes on.
type MissingError ¶
type MissingError struct{ Cases []string }
MissingError is a merge that lacks a record for declared cases.
func (*MissingError) Error ¶
func (e *MissingError) Error() string
type Options ¶
type Options struct {
Root string // checkout root; the models are root/tla
Cases []Case // the selected cases, in order
Jar Jar // the TLC jar
Java string // the java program
JavaVer string // the version java reported (JavaVersion); recorded
Out string // output directory: logs, RUNS.tsv and the private copy of the models
Budget time.Duration // the whole suite's limit
Workers int // TLC workers for a case expected to pass; counterexample cases use one
Manual bool // mode=manual in the records
Platform string // the platform label recorded in the host column (Platform)
CPUs int // logical CPUs of the machine, recorded
Clock func() time.Time // time.Now when nil
Exec Executor // Execute when nil
OnCase func(Record) // called with each record as it is made
// Selection is how Cases was chosen from the plan. RunSuite chooses again
// from the plan its digest names, runs that, and refuses when it is not the
// caller's Cases. The zero value selects every case.
Selection Selection
// contains filtered or unexported fields
}
Options is one suite: the selected cases under one budget.
type Outcome ¶
type Outcome struct {
Completed bool // "Model checking completed. No error has been found."
Generated string // states generated, digits only; "-" when TLC printed none
Distinct string // distinct states found, digits only; "-" when TLC printed none
Violations []Violation
// InitialState is set when an invariant is violated by the initial state.
// TLC stops there and prints no state count; the state it prints is the
// one it examined, so Generated and Distinct are 1 and 1.
InitialState bool
}
Outcome is what one TLC output says, apart from its exit status.
func Parse ¶
Parse reads a TLC output. The statistics are the LAST pair printed: TLC prints a progress line for every minute of a long run and the totals at the end, and the totals are the number a record keeps.
func (Outcome) TemporalViolations ¶
TemporalViolations returns the temporal violations TLC reported.
type Record ¶
type Record struct {
Config string
Module string
InputSHA256 string // fingerprint of what the case reads (Source.Inputs, Digest)
InputFiles int // how many inputs the fingerprint covers
JarSHA256 string
JavaVersion string // the version java reported, as JavaVersion reads it
Host string // the platform label of the machine that ran TLC (Platform), never a machine name
CPUs int // logical CPUs of that machine
StartedUTC string // RFC 3339, microseconds, +00:00
Workers int // TLC workers this case ran with
Generated string // states generated; "-" when unknown
Distinct string // distinct states; "-" when unknown
Seconds string // elapsed, three decimals
Exit int
Result string // PASS or FAIL
Expected string
Property string
Budget string // seconds, shortest form
Mode string // bounded or manual
}
Record is one measured case, one row of tla/RUNS.tsv.
func Merge ¶
Merge joins the records of several runs (one per group) into the complete set, in the order of the case plan. It refuses a record for a case the plan does not declare, a case measured twice, a record whose fingerprint is not the one src gives its case now (measured on other models, another plan row or another runner than these: a merge of a stale run and a fresh one is a mixture no fingerprint describes), and a declared case that has no record.
func ReadRecords ¶
ReadRecords reads a records file and refuses a header that is not the current layout (naming the layout it found and the one expected), a short row, and a count or exit cell that is not a plain integer (no trailing text, sign or leading zero).
func ReadRecordsFile ¶
ReadRecordsFile reads the records at path.
type Result ¶
type Result struct {
Records []Record
Failed bool // a case was not the declared result, or the budget ran out first
Refused string // set when the records were not written, and why
Work string // the private copy of the models the cases ran in
}
Result is what a suite did.
func RunSuite ¶
RunSuite runs the selected cases one after the other. Each runs in a private copy of the models, with its own temporary directory for TLC's standard modules and state files, and its log at Out/<config>.log. When the cases are done the fingerprint of each is taken again and the records are written to Out/RUNS.tsv only if none changed; a suite whose inputs moved under it writes nothing and says so. A budget that ends before the last case is a failure, and the records of the cases that ran are still written.
type Run ¶
type Run struct {
Java string // the java program
Jar string // the TLC jar
Dir string // working directory: the private copy of the models
JVM []string // JVM flags before -cp, for example -Xmx2g
TmpDir string // java.io.tmpdir, when not empty: TLC unpacks its standard modules there
Workers int // TLC -workers
LnCheckFinal bool // -lncheck final: check liveness once at the end
NoDeadlock bool // -deadlock: switch TLC's deadlock check OFF
MetaDir string // -metadir, when not empty: TLC's state files
Config string // -config
Module string // the .tla file
}
Run is one TLC invocation: the java flags, the TLC flags and the module.
type Source ¶
type Source struct {
TLADir string // root/tla, or a copy of it
Plan []byte // the bytes of tla/CASES.tsv
Runner map[string][]byte // the runner's files by path under the checkout root
}
Source is where the inputs of a case are read from: the directory that holds its configuration and modules, the bytes of the case plan and the runner's files by path under the checkout root. Reading them apart lets a suite hold the private copy of the models to the fingerprint of the checkout's, and lets internal/ci hold the runner's embedded bytes to the ones on disk.
func SourceAt ¶
SourceAt reads the case plan of root/tla and takes the runner from the bytes this binary was built with.
func (Source) Fingerprint ¶
Fingerprint is the digest of a case's inputs and the number of files it covers.
func (Source) Inputs ¶
Inputs is exactly what a TLC run of the case reads, sorted by path: its configuration; the module the plan names for it and, transitively, every module that one extends or instantiates (a name with no file under tla/ must be one of TLC's standard modules); the case's own row of the plan under the plan's header; and the runner's result files (ResultFiles). It is an error when the case is not in the plan, when the configuration or a module cannot be read, or when a module names one that is neither a file nor a standard module.
The jar is not an input: a record names it in its own column.
Source Files