README
¶
migo
JorgeGCoelho/migo is a MiGo Types library in Go.
This library is a fork of a fork of the original MiGo Types library with minor adjustments, for my project GoDDaR MiGo (mini-go) is a calculus introduced in this paper to capture core concurrency features of Go. It was later extended to account for shared memory primitives in an ongoing publication, by including GoldyLocks, a calculus centered around shared memory (relative paper currently accepted at ECOOP 2020 and to be linked here when available).
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.
It has been extended, with the help of the original author, to capture shared memory primitives such as shared variables and mutual exclusion (Mutex) locks.
Install
The package can be installed using go get:
go get github.com/jujuyuki/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
;
mutprefix = "lock" identifier
| "unlock" identifier
;
rwmutprefix = mutprefix
| "rlock" identifier
| "runlock" identifier
;
def-stmt = "let" identifier = "newchan" identifier, digit+ ";"
| prefix ";"
| "letmem" identifier ";"
| memprefix ";"
| "letsync" identifier "mutex;"
| mutprefix ";"
| "letsync" identifier "rwmutex;"
| rwmutprefix ";"
| "close" identifier ";"
| "call" identifier "(" params ")" ";"
| "spawn" identifier "(" params ")" ";"
| "if" def-stmt+ "else" def-stmt+ "endif" ";"
| "select" ( "case" prefix ";" def-stmt* )* "endselect" ";"
;
Verification of MiGo
Godel2 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 ¶
- Variables
- func CalleeParameterString(params []*Parameter) string
- func CallerParameterString(params []*Parameter) string
- type CallStatement
- type CloseStatement
- type Function
- func (f *Function) AddParams(params ...*Parameter)
- func (f *Function) AddStmts(stmts ...Statement)
- func (f *Function) GetParamByCalleeValue(v NamedVar) (*Parameter, error)
- func (f *Function) IsEmpty() bool
- func (f *Function) PutAway()
- func (f *Function) Restore() ([]Statement, error)
- func (f *Function) SimpleName() string
- func (f *Function) String() string
- type IfForStatement
- type IfStatement
- type MemRead
- type MemWrite
- type NamedVar
- type NewChanStatement
- type NewMem
- type NewSyncMutex
- type NewSyncRWMutex
- type Parameter
- type Program
- type RecvStatement
- type SelectStatement
- type SendStatement
- type SpawnStatement
- type Statement
- type StmtsStack
- type SyncMutexLock
- type SyncMutexUnlock
- type SyncRWMutexRLock
- type SyncRWMutexRUnlock
- type TauStatement
Examples ¶
Constants ¶
This section is empty.
Variables ¶
var ( // ErrEmptyStack is the error message if the Statement stack is empty. ErrEmptyStack = errors.New("stack: empty") )
Functions ¶
func CalleeParameterString ¶
CalleeParameterString converts a slice of *Parameter to parameter string.
func CallerParameterString ¶
CallerParameterString converts a slice of *Parameter to parameter string.
Types ¶
type CallStatement ¶
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 ¶
NewFunction creates a new Function using the given name.
func (*Function) AddParams ¶
AddParams adds Parameters to Function.
If Parameter already exists this does nothing.
func (*Function) GetParamByCalleeValue ¶
GetParamByCalleeValue is for looking up params from the body of a Function.
func (*Function) SimpleName ¶
SimpleName returns a filtered name of a function.
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 ¶
IfStatement is a conditional statement.
IfStatements always have both Then and Else.
func (*IfStatement) String ¶
func (s *IfStatement) String() string
type NewChanStatement ¶
NewChanStatement creates and names a newly created channel.
func (*NewChanStatement) String ¶
func (s *NewChanStatement) String() string
type NewMem ¶
type NewMem struct {
Name NamedVar
}
NewMem creates a new memory or variable reference.
type NewSyncMutex ¶
type NewSyncMutex struct {
Name NamedVar
}
NewSyncMutex is a sync.Mutex initialisation statement.
func (*NewSyncMutex) String ¶
func (m *NewSyncMutex) String() string
type NewSyncRWMutex ¶
type NewSyncRWMutex struct {
Name NamedVar
}
NewSyncRWMutex is a sync.RWMutex initialisation statement.
func (*NewSyncRWMutex) String ¶
func (m *NewSyncRWMutex) 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 (*Program) AddFunction ¶
AddFunction adds a Function to Program.
If Function already exists this does nothing.
type RecvStatement ¶
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 ¶
SendStatement sends to Chan.
func (*SendStatement) String ¶
func (s *SendStatement) String() string
type SpawnStatement ¶
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 StmtsStack ¶
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 (*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
Source Files
Directories
¶
| Path | Synopsis |
|---|---|
|
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. |
|
Package parser is a parser for MiGo (mini-go calculus) types.
|
Package parser is a parser for MiGo (mini-go calculus) types. |