migo

package module
Version: v4.0.1 Latest Latest
Warning

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

Go to latest
Published: Mar 26, 2020 License: Apache-2.0 Imports: 6 Imported by: 0

README

migo Build Status GoDoc

nickng/migo is a MiGo Types library in Go.

MiGo (mini-go) calculus is a introduced in this paper to capture core concurrency features of Go.

This library was designed to work with MiGo types, i.e. the types of communication primitives in the MiGo calculus, where the values to be sent/received are abstracted away, for static analysis and verification.

Install

The package can be installed using go get:

go get github.com/nickng/migo

MiGo types

Syntax:

identifier = [a-zA-Z0-9_.,#/]
digit      = [0-9]
program    = definition* ;
definition = "def " identifier "(" param ")" ":" def-body ;
param      =
           | params
           ;
params     = identifier
           | params "," identifier
           ;
def-body   = def-stmt+
           ;
prefix     = "send" identifier
           | "recv" identifier
           | "tau"
           ;
memprefix  = "read"  identifier
           | "write" identifier
           ;
def-stmt   = "let" identifier = "newchan" identifier, digit+ ";"
           | prefix ";"
           | "letmem" identifier ";"
           | memprefix ";"
           | "close" identifier ";"
           | "call"  identifier "(" params ")" ";"
           | "spawn" identifier "(" params ")" ";"
           | "if" def-stmt+ "else" def-stmt+ "endif" ";"
           | "select" ( "case" prefix ";" def-stmt* )* "endselect" ";"
           ;

Verification of MiGo

Gong is a liveness and safety checker of MiGo types. The tool accepts MiGo types format generated by this package.

Documentation

Overview

Package migo is a library for working with MiGo (mini-go calculus) types. MiGo is a process calculi/type that captures the core concurrency features of Go.

MiGo types syntax

This is the output format of MiGo Types in EBNF.

identifier = [a-zA-Z0-9_.,#/]
digit      = [0-9]
program    = definition* ;
definition = "def " identifier "(" param ")" ":" def-body ;
param      =
           | params
           ;
params     = identifier
           | params "," identifier
           ;
def-body   = def-stmt+
           ;
prefix     = "send" identifier
           | "recv" identifier
           | "tau"
           ;
memprefix  = "read"  identifier
           | "write" identifier
           ;
def-stmt   = "let" identifier = "newchan" identifier, digit+ ";"
           | prefix ";"
           | "letmem" identifier ";"
           | memprefix ";"
           | "close" identifier ";"
           | "call"  identifier "(" params ")" ";"
           | "spawn" identifier "(" params ")" ";"
           | "if" def-stmt+ "else" def-stmt+ "endif" ";"
           | "select" ( "case" prefix ";" def-stmt* )* "endselect" ";"
           ;

A MiGo type can be obtained by calling String() function of the Program, see examples below.

p := NewProgram()
// ... add functions
migoType := p.String()

Index

Examples

Constants

This section is empty.

Variables

View Source
var (
	// ErrEmptyStack is the error message if the Statement stack is empty.
	ErrEmptyStack = errors.New("stack: empty")
)

Functions

func CalleeParameterString

func CalleeParameterString(params []*Parameter) string

CalleeParameterString converts a slice of *Parameter to parameter string.

func CallerParameterString

func CallerParameterString(params []*Parameter) string

CallerParameterString converts a slice of *Parameter to parameter string.

Types

type CallStatement

type CallStatement struct {
	Name   string
	Params []*Parameter
}

CallStatement captures function calls or block jumps in the SSA.

func (*CallStatement) AddParams

func (s *CallStatement) AddParams(params ...*Parameter)

AddParams add parameter(s) to a Function call.

func (*CallStatement) SimpleName

func (s *CallStatement) SimpleName() string

SimpleName returns a filtered name.

func (*CallStatement) String

func (s *CallStatement) String() string

type CloseStatement

type CloseStatement struct {
	Chan string // Channel name
}

CloseStatement closes a channel.

func (*CloseStatement) String

func (s *CloseStatement) String() string

type Function

type Function struct {
	Name    string       // Name of the function.
	Params  []*Parameter // Parameters (map from local variable name to Parameter).
	Stmts   []Statement  // Function body (slice of statements).
	HasComm bool         // Does the function has communication statement?
	// contains filtered or unexported fields
}

Function is a block of Statements sharing the same parameters.

func NewFunction

func NewFunction(name string) *Function

NewFunction creates a new Function using the given name.

func (*Function) AddParams

func (f *Function) AddParams(params ...*Parameter)

AddParams adds Parameters to Function.

If Parameter already exists this does nothing.

func (*Function) AddStmts

func (f *Function) AddStmts(stmts ...Statement)

AddStmts add Statement(s) to a Function.

func (*Function) GetParamByCalleeValue

func (f *Function) GetParamByCalleeValue(v NamedVar) (*Parameter, error)

GetParamByCalleeValue is for looking up params from the body of a Function.

func (*Function) IsEmpty

func (f *Function) IsEmpty() bool

IsEmpty returns true if the Function body is empty.

func (*Function) PutAway

func (f *Function) PutAway()

PutAway pushes current statements to stack.

func (*Function) Restore

func (f *Function) Restore() ([]Statement, error)

Restore pops current statements from stack.

func (*Function) SimpleName

func (f *Function) SimpleName() string

SimpleName returns a filtered name of a function.

func (*Function) String

func (f *Function) String() string

type IfForStatement

type IfForStatement struct {
	ForCond string // Condition of the loop
	Then    []Statement
	Else    []Statement
}

IfForStatement is a conditional statement introduced by a for-loop.

IfForStatements always have both Then and Else.

func (*IfForStatement) String

func (s *IfForStatement) String() string

type IfStatement

type IfStatement struct {
	Then []Statement
	Else []Statement
}

IfStatement is a conditional statement.

IfStatements always have both Then and Else.

func (*IfStatement) String

func (s *IfStatement) String() string

type MemRead

type MemRead struct {
	Name string
}

MemRead is a memory read statement.

func (*MemRead) String

func (s *MemRead) String() string

type MemWrite

type MemWrite struct {
	Name string
}

MemWrite is a memory write statement.

func (*MemWrite) String

func (s *MemWrite) String() string

type NamedVar

type NamedVar interface {
	Name() string
	String() string
}

NamedVar is a named variable.

type NewChanStatement

type NewChanStatement struct {
	Name NamedVar
	Chan string
	Size int64
}

NewChanStatement creates and names a newly created channel.

func (*NewChanStatement) String

func (s *NewChanStatement) String() string

type NewMem

type NewMem struct {
	Name string
}

NewMem creates a new memory or variable reference.

func (*NewMem) String

func (s *NewMem) String() string

type NewSyncMutex

type NewSyncMutex struct {
	Name string
}

NewSyncMutex is a sync.Mutex initialisation statement.

func (*NewSyncMutex) String

func (m *NewSyncMutex) String() string

type NewSyncRWMutex

type NewSyncRWMutex struct {
	Name string
}

NewSyncRWMutex is a sync.RWMutex initialisation statement.

func (*NewSyncRWMutex) String

func (m *NewSyncRWMutex) String() string

type Parameter

type Parameter struct {
	Caller NamedVar
	Callee NamedVar
}

Parameter is a translation from caller environment to callee.

func (*Parameter) String

func (p *Parameter) String() string

type Program

type Program struct {
	Funcs []*Function // Function definitions.
	// contains filtered or unexported fields
}

Program is a set of Functions in a program.

Example

The example demonstrates the usage of the migo API for building MiGo programs.

p := migo.NewProgram()
f := migo.NewFunction("F")
SendXStmt := &migo.SendStatement{Chan: "x"}                              // send x
callGStmt := &migo.CallStatement{Name: "G", Params: []*migo.Parameter{}} // call G()
f.AddStmts(SendXStmt, callGStmt)                                         // F()
g := migo.NewFunction("G")
g.AddParams()                    // G()
g.AddStmts(&migo.TauStatement{}) // tau
p.AddFunction(f)
p.AddFunction(g)
fmt.Print(p.String())
Output:

def F():
    send x;
    call G();
def G():
    tau;

func NewProgram

func NewProgram() *Program

NewProgram creates a new empty Program.

func (*Program) AddFunction

func (p *Program) AddFunction(f *Function)

AddFunction adds a Function to Program.

If Function already exists this does nothing.

func (*Program) Function

func (p *Program) Function(name string) (*Function, bool)

Function gets a Function in a Program by name.

Returns the function and a bool indicating whether lookup was successful.

func (*Program) String

func (p *Program) String() string

type RecvStatement

type RecvStatement struct {
	Chan string
}

RecvStatement receives from Chan.

func (*RecvStatement) String

func (s *RecvStatement) String() string

type SelectStatement

type SelectStatement struct {
	Cases [][]Statement
}

SelectStatement is non-deterministic choice

func (*SelectStatement) String

func (s *SelectStatement) String() string

type SendStatement

type SendStatement struct {
	Chan string
}

SendStatement sends to Chan.

func (*SendStatement) String

func (s *SendStatement) String() string

type SpawnStatement

type SpawnStatement struct {
	Name   string
	Params []*Parameter
}

SpawnStatement captures spawning of goroutines.

func (*SpawnStatement) AddParams

func (s *SpawnStatement) AddParams(params ...*Parameter)

AddParams add parameter(s) to a goroutine spawning Function call.

func (*SpawnStatement) SimpleName

func (s *SpawnStatement) SimpleName() string

SimpleName returns a filtered name.

func (*SpawnStatement) String

func (s *SpawnStatement) String() string

type Statement

type Statement interface {
	String() string
}

Statement is a generic statement.

type StmtsStack

type StmtsStack struct {
	sync.Mutex
	// contains filtered or unexported fields
}

StmtsStack is a stack of []Statement.

StmtsStack is mostly used for building nested control-flow of the MiGo language.

Example
b := []migo.Statement{}
s := migo.NewStmtsStack() // Create a new stack
s.Push(b)                 // Push to empty stack
b, err := s.Pop()         // Pop from stack (stack is empty again)
if err != nil {
	fmt.Println("error:", err)
}
Output:

func NewStmtsStack

func NewStmtsStack() *StmtsStack

NewStmtsStack creates a new StmtsStack.

func (*StmtsStack) IsEmpty

func (s *StmtsStack) IsEmpty() bool

IsEmpty returns true if stack is empty.

func (*StmtsStack) Pop

func (s *StmtsStack) Pop() ([]Statement, error)

Pop removes and returns a Statement from top of stack.

func (*StmtsStack) Push

func (s *StmtsStack) Push(stmt []Statement)

Push adds a new Statement to the top of stack.

func (*StmtsStack) Size

func (s *StmtsStack) Size() int

Size returns the number of elements in stack.

type SyncMutexLock

type SyncMutexLock struct {
	Name string
}

SyncMutexLock is a sync.Mutex Lock statement.

func (*SyncMutexLock) String

func (m *SyncMutexLock) String() string

type SyncMutexUnlock

type SyncMutexUnlock struct {
	Name string
}

SyncMutexUnlock is a sync.Mutex Unlock statement.

func (*SyncMutexUnlock) String

func (m *SyncMutexUnlock) String() string

type SyncRWMutexRLock

type SyncRWMutexRLock struct {
	Name string
}

SyncRWMutexRLock is a sync.RWMutex RLock statement.

func (*SyncRWMutexRLock) String

func (m *SyncRWMutexRLock) String() string

type SyncRWMutexRUnlock

type SyncRWMutexRUnlock struct {
	Name string
}

SyncRWMutexRUnlock is a sync.RWMutex RUnlock statement.

func (*SyncRWMutexRUnlock) String

func (m *SyncRWMutexRUnlock) String() string

type TauStatement

type TauStatement struct{}

TauStatement is inaction.

func (*TauStatement) String

func (s *TauStatement) String() string

Directories

Path Synopsis
Package parser is a parser for MiGo (mini-go calculus) types.
Package parser is a parser for MiGo (mini-go calculus) types.
internal
ctrlflow
Package ctrlflow represents and constructs control-flow graph (CFG) of MiGo functions in a MiGo program.
Package ctrlflow represents and constructs control-flow graph (CFG) of MiGo functions in a MiGo program.
passes/deadcall
Package deadcall defines a transformation pass to remove dead function calls.
Package deadcall defines a transformation pass to remove dead function calls.
passes/taufunc
Package taufunc defines a transformation pass to remove τ functions.
Package taufunc defines a transformation pass to remove τ functions.
passes/unused
Package unused defines a transformation pass to remove unused functions.
Package unused defines a transformation pass to remove unused functions.

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
t or T : Toggle theme light dark auto
y or Y : Canonical URL