distsys

package module
v0.0.0-...-2e7796a Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Apr 6, 2023 License: Apache-2.0 Imports: 11 Imported by: 7

Documentation

Index

Constants

This section is empty.

Variables

View Source 
var ErrArchetypeResourceLeafIndexed = errors.New("internal error: attempted to index a leaf archetype resource")
View Source 
var ErrArchetypeResourceMapReadWrite = errors.New("internal error: attempted to read/write a map archetype resource")
View Source 
var ErrAssertionFailed = errors.New("assertion failed")

ErrAssertionFailed will be returned by an archetype function in the generated code if an assertion fails.

View Source 
var ErrCriticalSectionAborted = errors.New("MPCal critical section aborted")

ErrCriticalSectionAborted it may be returned by any resource operations that can return an error. If it is returned the critical section that was performing that operation will be rolled back and canceled.

View Source 
var ErrDone = errors.New("a pseudo-error to indicate an archetype has terminated execution normally")

ErrDone exists only to be returned by archetype code implementing the Done label

View Source 
var ErrProcedureFallthrough = errors.New("control has reached the end of a procedure body without reaching a return")

ErrProcedureFallthrough indicated an archetype reached the Error label, and crashed.

Functions

This section is empty.

Types

type ArchetypeInterface 

type ArchetypeInterface struct {
	// contains filtered or unexported fields
}

ArchetypeInterface provides an archetype-centric interface to an MPCalContext. While just an opaque wrapper for an MPCalContext, it provides a separation of concerns between: (1) how to configure and run and MPCal archetype (available via a plain MPCalContext) (2) how the MPCal archetype's code accesses its configuration and internal state while running (available via ArchetypeInterface)

func (ArchetypeInterface) Call 

func (iface ArchetypeInterface) Call(procName string, returnPC string, argVals ...tla.Value) error

Call performs all necessary steps of a procedure call in MPCal, given a procedure name, a program counter to return to, and any number of arguments. Specifically, this involves: - read the callee's locals, and saving them onto the stack state variable - write the new argument values (argVals, in the same order as in MPCal) to the callee's arguments - initialize any local state variables in the callee - jump to the callee's first label via Goto

This method should be called at the end of a critical section.

func (ArchetypeInterface) EnsureArchetypeResourceLocal 

func (iface ArchetypeInterface) EnsureArchetypeResourceLocal(name string, value tla.Value)

EnsureArchetypeResourceLocal ensures that a local state variable exists (local to an archetype or procedure), creating it with the given default value if not.

func (ArchetypeInterface) GetConstant 

func (iface ArchetypeInterface) GetConstant(name string) func(args ...tla.Value) tla.Value

GetConstant returns the constant operator bound to the given name as a variadic Go function. The function is generated in DefineConstantOperator, and is expected to check its own arguments.

func (ArchetypeInterface) Goto 

func (iface ArchetypeInterface) Goto(target string) error

Goto sets the running archetype's program counter to the target value. It will panic if the target is not a valid label name. This method should be called at the end of a critical section.

func (ArchetypeInterface) NextFairnessCounter 

func (iface ArchetypeInterface) NextFairnessCounter(id string, ceiling uint) uint

NextFairnessCounter returns number [0,ceiling) indicating a non-deterministic branching decision which, given an MPCal critical section being retried indefinitely with no other changes, will try to guarantee that all possible non-deterministic branch choices will be attempted.

func (ArchetypeInterface) Read 

func (iface ArchetypeInterface) Read(handle ArchetypeResourceHandle, indices []tla.Value) (value tla.Value, err error)

Read models the MPCal expression resourceFromHandle[indices...]. If is expected to be called only from PGo-generated code.

func (ArchetypeInterface) ReadArchetypeResourceLocal 

func (iface ArchetypeInterface) ReadArchetypeResourceLocal(name string) tla.Value

ReadArchetypeResourceLocal is a short-cut to reading a local state variable, which, unlike other resources, is statically known to not require any critical section management. It will return the resource's value as-is, and will crash if the named resource isn't exactly a local state variable.

func (ArchetypeInterface) RequireArchetypeResource 

func (iface ArchetypeInterface) RequireArchetypeResource(name string) ArchetypeResourceHandle

RequireArchetypeResource returns a handle to the archetype resource with the given name. It panics if this resource does not exist.

func (ArchetypeInterface) RequireArchetypeResourceRef 

func (iface ArchetypeInterface) RequireArchetypeResourceRef(name string) (ArchetypeResourceHandle, error)

RequireArchetypeResourceRef returns a handle to the archetype resource with the given name, when the name refers to a resource that was passed by ref in MPCal (in Go, ref-passing has an extra indirection that must be followed). If the resource does not exist, or an invalid indirection is used, this method will panic.

func (ArchetypeInterface) Return 

func (iface ArchetypeInterface) Return() error

Return executes the entire semantics of an MPCal procedure return. This involves: - popping a record from top-of-stack (which must not be empty), which contains many pairs of name -> TLA+ value

  • for each pair, find the resource with the given name, and write the given TLA+ value to it

This ensures all the callee's local state variables have their values restored to how they were before the procedure call. The program counter, with the label to return to, is included in the state variables to "restore", so no special logic is needed for that.

This method should be called at the end of a critical section.

func (ArchetypeInterface) Self 

func (iface ArchetypeInterface) Self() tla.Value

Self returns the associated archetype's self binding. Requires a configured archetype.

func (ArchetypeInterface) TailCall 

func (iface ArchetypeInterface) TailCall(procName string, argVals ...tla.Value) error

TailCall specialises the Call operation via the well-known tail-call optimisation. It does this by: - extracting a return value from the top of the callstack - performing a Return - immediately performing a Call to procName with argVals and the extracted return destination

This ensures that the existing top-of-stack is cleaned up, the correct return address is stored, and all the procedure call semantics for a new call replacing the current one are satisfied.

Note: like Return, this should never be called outside a procedure, as it relies on an existing stack frame.

This method, like those it wraps, should be called at the end of a critical section.

func (ArchetypeInterface) Write 

func (iface ArchetypeInterface) Write(handle ArchetypeResourceHandle, indices []tla.Value, value tla.Value) (err error)

Write models the MPCal statement resourceFromHandle[indices...] := value. It is expected to be called only from PGo-generated code.

type ArchetypeResource 

type ArchetypeResource interface {
	// Abort will be called when the resource should be reset to a state similar to the last Commit.
	// May return nil. If it doesn't return nil, the channel should notify one time, when the operation is complete.
	// If it returns nil, the operation is considered complete immediately.
	Abort() chan struct{}
	// PreCommit will be called after any number of ReadValue, WriteValue, or Index operations.
	// It signals if it is reasonable to go ahead with a Commit.
	// If the resource might need to back out, it should do it here.
	// May return nil. If it doesn't return nil, the channel should yield one error value. If the error is nil,
	// Commit may go ahead. Otherwise, it may not.
	// Returning nil is considered a short-cut to immediately yielding a nil error.
	PreCommit() chan error
	// Commit will be called if no sibling PreCommit calls raised any errors.
	// It must unconditionally commit current resource state. By necessity, this is the only resource operation that
	// may block indefinitely.
	// May return nil. If it doesn't return nil, the channel should notify once the commit is complete.
	// Returning nil is considered as an immediately successful commit.
	Commit() chan struct{}
	// ReadValue must return the resource's current value.
	// If the resource is not ready, ErrCriticalSectionAborted may be returned alongside a default Value.
	// This operation should not block indefinitely.
	// This makes no sense for a map-like resource, and should be blocked off with ArchetypeResourceMapMixin in that case.
	ReadValue() (tla.Value, error)
	// WriteValue must update the resource's current value.
	// It follows the same conventions as ReadValue.
	WriteValue(value tla.Value) error
	// Index must return the resource's sub-resource at the given index.
	// It's unclear when this would be needed, but, if the resource is not ready, then this operation may return
	// ErrCriticalSectionAborted.
	// This makes no sense for a value-like resource, and should be blocked off with ArchetypeResourceLeafMixin in that case.
	Index(index tla.Value) (ArchetypeResource, error)
	// Close will be called when the archetype stops running (as a result, it's
	// not in the middle of a critical section). Close stops running of any
	// background jobs and cleans up the stuff that no longer needed when the
	// archetype is not running. Close will be called at most once by an MPCal
	// Context.
	Close() error
	// VClockHint allows the resource to transform the archetype's current vector clock, which can be used by the
	// archetype resource to indicate causality information.
	// This method will be called twice per critical section, between PreCommit and Commit, in order to allow the resource
	// implementation to both add its information to the current vector clock, and to learn the critical section's final
	// clock information.
	// This optional method has default implementations for both the leaf and map mixins which do nothing.
	VClockHint(archClock trace.VClock) trace.VClock
}

ArchetypeResource represents an interface between an MPCal model and some external environment. Such a resource should be instantiated under the control of MPCalContext.EnsureArchetypeResource. Many implementations are available under ./resources. This API describes what is expected of those implementations, and any others.

type ArchetypeResourceHandle 

type ArchetypeResourceHandle string

ArchetypeResourceHandle encapsulates a reference to an ArchetypeResource. These handles insulate the end-user from worrying about the specifics of resource lifetimes, logging, and crash recovery scenarios.

type ArchetypeResourceLeafMixin 

type ArchetypeResourceLeafMixin struct{}

func (ArchetypeResourceLeafMixin) Index 

func (ArchetypeResourceLeafMixin) Index(tla.Value) (ArchetypeResource, error)

func (ArchetypeResourceLeafMixin) VClockHint 

func (ArchetypeResourceLeafMixin) VClockHint(archClock trace.VClock) trace.VClock

type ArchetypeResourceMapMixin 

type ArchetypeResourceMapMixin struct{}

func (ArchetypeResourceMapMixin) ReadValue 

func (ArchetypeResourceMapMixin) ReadValue() (tla.Value, error)

func (ArchetypeResourceMapMixin) VClockHint 

func (ArchetypeResourceMapMixin) VClockHint(archClock trace.VClock) trace.VClock

func (ArchetypeResourceMapMixin) WriteValue 

func (ArchetypeResourceMapMixin) WriteValue(tla.Value) error

type FairnessCounter 

type FairnessCounter interface {
	// BeginCriticalSection will be called once per critical section, and should
	// contain any necessary set-up for that critical section's execution.
	BeginCriticalSection(pc string)
	// NextFairnessCounter may be called repeatedly within a critical section,
	// with distinct ids per distinct branching point.
	NextFairnessCounter(id string, ceiling uint) uint
}

FairnessCounter is an abstraction over policies for MPCal's non-deterministic branch selection. See ArchetypeInterface.NextFairnessCounter.

func MakeRoundRobinFairnessCounter 

func MakeRoundRobinFairnessCounter() FairnessCounter

MakeRoundRobinFairnessCounter produces a FairnessCounter that follows a round-robin pattern. This process is similar to BigInt incrementation, but also tracking branch identifiers and trying to be robust to changes in the ceiling value (which may happen if we are exploring selections from a set whose cardinality changes).

type LocalArchetypeResource 

type LocalArchetypeResource struct {
	// contains filtered or unexported fields
}

LocalArchetypeResource is a bare-bones resource that just holds and buffers a Value.

func NewLocalArchetypeResource 

func NewLocalArchetypeResource(value tla.Value) *LocalArchetypeResource

func (*LocalArchetypeResource) Abort 

func (res *LocalArchetypeResource) Abort() chan struct{}

func (*LocalArchetypeResource) Close 

func (res *LocalArchetypeResource) Close() error

func (*LocalArchetypeResource) Commit 

func (res *LocalArchetypeResource) Commit() chan struct{}

func (*LocalArchetypeResource) GetState 

func (res *LocalArchetypeResource) GetState() ([]byte, error)

func (*LocalArchetypeResource) Index 

func (res *LocalArchetypeResource) Index(index tla.Value) (ArchetypeResource, error)

Index is a special case: a local resource uniquely _can_ be indexed and read/written interchangeably! See comment on localArchetypeSubResource

func (*LocalArchetypeResource) PreCommit 

func (res *LocalArchetypeResource) PreCommit() chan error

func (*LocalArchetypeResource) ReadValue 

func (res *LocalArchetypeResource) ReadValue() (tla.Value, error)

func (*LocalArchetypeResource) VClockHint 

func (res *LocalArchetypeResource) VClockHint(archClock trace.VClock) trace.VClock

func (*LocalArchetypeResource) WriteValue 

func (res *LocalArchetypeResource) WriteValue(value tla.Value) error

type MPCalArchetype 

type MPCalArchetype struct {
	Name                                 string                         // the archetype's name, as it reads in the MPCal source code
	Label                                string                         // the full label name of the first critical section this archetype should execute
	RequiredRefParams, RequiredValParams []string                       // names of ref and non-ref parameters
	JumpTable                            MPCalJumpTable                 // a cross-reference to a jump table containing this archetype's critical sections
	ProcTable                            MPCalProcTable                 // a cross-reference to a table of all MPCal procedures this archetype might call
	PreAmble                             func(iface ArchetypeInterface) // called on archetype start-up, this code should initialize any local variables the archetype has
}

MPCalArchetype holds all the metadata necessary to run an archetype, aside from user-provided configuration

type MPCalContext 

type MPCalContext struct {
	// contains filtered or unexported fields
}

MPCalContext manages the internal lifecycle of a compiled MPCal model's execution. This includes: - critical section state - configured resources, constant values, and the archetype's self binding - the ability to start and stop the archetype, via Run and Close.

func NewMPCalContext 

func NewMPCalContext(self tla.Value, archetype MPCalArchetype, configFns ...MPCalContextConfigFn) *MPCalContext

NewMPCalContext is the principal function for creating MPCalContext instances. It returns a fully-constructed context, executing configuration steps internally. The self parameter refers to the archetype's "self" binding, and should be an appropriately unique TLA+ value, with the same semantics as used in PlusCal and TLC. The archetype parameter should refer to a static PGo-compiled structure, which contains all intrinsic information about how a given archetype should run. This information includes: - necessary value-level archetype parameters (no ref keyword) - necessary archetype resources (with ref keyword, and with or without [_]) - control flow information, pointers to routines for the relevant critical sections

See MPCalArchetype for further information.

For information on both necessary and optional configuration, see MPCalContextConfigFn, which can be provided to NewMPCalContext in order to set constant values, pass archetype parameters, and any other configuration information.

func NewMPCalContextWithoutArchetype 

func NewMPCalContextWithoutArchetype(configFns ...MPCalContextConfigFn) *MPCalContext

NewMPCalContextWithoutArchetype creates an almost-uninitialized context, useful for calling pure TLA+ operators. The returned context will cause almost all operations to panic, except: - configuring constant definitions - passing the result of MPCalContext.IFace() to a plain TLA+ operator

func (*MPCalContext) Archetype 

func (ctx *MPCalContext) Archetype() MPCalArchetype

func (*MPCalContext) IFace 

func (ctx *MPCalContext) IFace() ArchetypeInterface

IFace provides an ArchetypeInterface, giving access to methods considered MPCal-internal. This is useful when directly calling pure TLA+ operators using a context constructed via NewMPCalContextWithoutArchetype, and is one of very few operations that will work on such a context.

func (*MPCalContext) Run 

func (ctx *MPCalContext) Run() (err error)

Run will execute the archetype loaded into ctx. This routine assumes all necessary information (resources, constant definitions) have been pre-loaded, and encapsulates the entire archetype's execution.

This method may return the following outcomes (be sure to use errors.Is, see last point): - nil: the archetype reached the Done label, and has ended of its own accord with no issues - ErrAssertionFailed: an assertion in the MPCal code failed (this error will be wrapped by a string describing the assertion) - ErrProcedureFallthrough: the Error label was reached, which is an error in the MPCal code - one or more (possibly aggregated, possibly with one of the above errors) implementation-defined errors produced by failing resources

func (*MPCalContext) Stop 

func (ctx *MPCalContext) Stop()

Stop requests that the archetype running under this context exits, roughly like the POSIX interrupt signal. The archetype's execution will be pre-empted at the next label boundary or critical section retry. This function will block until the exit is complete, and all resources have been cleaned up. If the archetype has not started, this function will ensure that it does not, without waiting.

type MPCalContextConfigFn 

type MPCalContextConfigFn func(ctx *MPCalContext)

func DefineConstantOperator 

func DefineConstantOperator(name string, defn interface{}) MPCalContextConfigFn

DefineConstantOperator is a more generic form of DefineConstantValue, which allows the specification of higher-order constants.

e.g: 

CONSTANT IM_SPECIAL(_, _)

The above example could be configured as such, if one wanted to approximate `IM_SPECIAL(a, b) == a + b`: 

		DefineConstantOperator("IM_SPECIAL", func(a, b Value) Value {
     	return ModulePlusSymbol(a, b)
     })

Note that the type of defn is interface{} in order to accommodate variadic functions, with reflection being used to determine the appropriate arity information. Any functions over Value, returning a single Value, are accepted. To match TLA+ semantics, the provided function should behave as effectively pure.

Valid inputs include: 

func() Value { ... }
func(a, b, c, Value) Value { ... }
func(variadic... Value) Value { ... }
func(a Value, variadic... Value) Value { ... }

func DefineConstantValue 

func DefineConstantValue(name string, value tla.Value) MPCalContextConfigFn

DefineConstantValue will bind a constant name to a provided TLA+ value. The name must match one of the constants declared in the MPCal module, for this option to make sense. Not all constants need to be defined, as long as they are not accessed at runtime.

func EnsureArchetypeRefParam 

func EnsureArchetypeRefParam(name string, res ArchetypeResource) MPCalContextConfigFn

EnsureArchetypeRefParam binds an ArchetypeResource to the provided name. The name must match one of the archetype's parameter names, and must refer to a ref parameter. Calling MPCalContext.Run while failing to meet these conditions will panic. The resource is provided via the res argument.

func EnsureArchetypeValueParam 

func EnsureArchetypeValueParam(name string, value tla.Value) MPCalContextConfigFn

EnsureArchetypeValueParam binds a Value to the provided name. The name must match one of the archetype's parameter names, and must not refer to a ref parameter. If these conditions are not met, attempting to call MPCalContext.Run will panic. Like with EnsureArchetypeRefParam, the provided value may not be used, if existing state has been recovered from storage.

func EnsureMPCalContextConfigs 

func EnsureMPCalContextConfigs(configs ...MPCalContextConfigFn) MPCalContextConfigFn

EnsureMPCalContextConfigs allows multiple MPCalContext configuration options to be treated as one. This is useful when there is a set of options common to several contexts, and you want a simple way to just "import" them into each configuration. Without this construct, something like a slice append() is needed, which makes the code harder to read and adds even more complexity to the already-complicated and deeply nested NewMPCalContext call. With this construct, you can just add the whole collection as a configuration option, and continue listing custom configuration as normal.

func SetFairnessCounter 

func SetFairnessCounter(fairnessCounter FairnessCounter) MPCalContextConfigFn

func SetTraceRecorder 

func SetTraceRecorder(recorder trace.Recorder) MPCalContextConfigFn

type MPCalCriticalSection 

type MPCalCriticalSection struct {
	Name string                               // the critical section's full name (in the form ArchetypeOrProcedureName.LabelName)
	Body func(iface ArchetypeInterface) error // code for executing this critical section. should be straight-line code that runs in a bounded amount of time.
}

MPCalCriticalSection holds metadata for a single MPCal critical section

type MPCalJumpTable 

type MPCalJumpTable map[string]MPCalCriticalSection

MPCalJumpTable is an immutable table of all critical sections a given collection of archetypes and procedures might jump to

func MakeMPCalJumpTable 

func MakeMPCalJumpTable(criticalSections ...MPCalCriticalSection) MPCalJumpTable

MakeMPCalJumpTable constructs a jump table from a sequence of MPCalCriticalSection records

type MPCalProc 

type MPCalProc struct {
	Name      string                               // the procedure's name, as given in the MPCal model
	Label     string                               // the fully qualified name of the procedure's first label
	StateVars []string                             // the fuly-qualified names of all the procedure's local state variables, including arguments and refs
	PreAmble  func(iface ArchetypeInterface) error // code to initialize local state variables, writing any initial values they might have. runs as part of a call to the procedure.
}

MPCalProc holds all metadata necessary for calling an MPCal procedure

type MPCalProcTable 

type MPCalProcTable map[string]MPCalProc

MPCalProcTable is an immutable table of all procedures a given collection of archetypes and procedures might call

func MakeMPCalProcTable 

func MakeMPCalProcTable(procs ...MPCalProc) MPCalProcTable

MakeMPCalProcTable constructs a table of procedure metadata from a sequence of MPCalProc

Source Files

View all Source files

Directories

Path Synopsis

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.