README
¶
migo 
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
Some tests uses golang/mock, to (re)generate mock files, install mockgen and
run go generate:
go get github.com/golang/mock/mockgen
go generate
go test
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"
;
def-stmt = "let" identifier = "newchan" identifier, digit ";"
| prefix ";"
| "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"
;
def-stmt = "let" identifier = "newchan" identifier, digit ";"
| prefix ";"
| "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 ¶
- Constants
- Variables
- func CalleeParameterString(params []*Parameter) string
- func CallerParameterString(params []*Parameter) string
- type CallStatement
- type CloseStatement
- type ConstToken
- type DigitsToken
- type ErrParse
- 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 IdentToken
- type IfStatement
- type Lexer
- type NamedVar
- type NewChanStatement
- type Parameter
- type Program
- type RecvStatement
- type Scanner
- type SelectStatement
- type SendStatement
- type SpawnStatement
- type Statement
- type StmtsStack
- type TauStatement
- type Tok
- type Token
- type TokenPos
Examples ¶
Constants ¶
const CALL = 57353
const CASE = 57355
const CLOSE = 57356
const COLON = 57351
const COMMA = 57346
const DEF = 57347
const DIGITS = 57368
const ELSE = 57357
const ENDIF = 57358
const ENDSELECT = 57359
const EQ = 57348
const IDENT = 57367
const IF = 57360
const LET = 57361
const LPAREN = 57349
const NEWCHAN = 57362
const RECV = 57365
const RPAREN = 57350
const SELECT = 57363
const SEMICOLON = 57352
const SEND = 57364
const SPAWN = 57354
const TAU = 57366
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 ConstToken ¶
type ConstToken struct {
// contains filtered or unexported fields
}
ConstToken is a normal constant token.
func (*ConstToken) EndPos ¶
func (t *ConstToken) EndPos() TokenPos
EndPos returns ending position of token.
func (*ConstToken) StartPos ¶
func (t *ConstToken) StartPos() TokenPos
StartPos returns starting position of token.
type DigitsToken ¶
type DigitsToken struct {
// contains filtered or unexported fields
}
DigitsToken is a token with numeric value (Digits).
func (*DigitsToken) EndPos ¶
func (t *DigitsToken) EndPos() TokenPos
EndPos returns ending position of token.
func (*DigitsToken) StartPos ¶
func (t *DigitsToken) StartPos() TokenPos
StartPos returns starting position of token.
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 IdentToken ¶
type IdentToken struct {
// contains filtered or unexported fields
}
IdentToken is a token with string value (Ident).
func (*IdentToken) EndPos ¶
func (t *IdentToken) EndPos() TokenPos
EndPos returns ending position of token.
func (*IdentToken) StartPos ¶
func (t *IdentToken) StartPos() TokenPos
StartPos returns starting position of token.
type IfStatement ¶
IfStatement is a conditional statement.
IfStatements always have both Then and Else.
func (*IfStatement) String ¶
func (s *IfStatement) String() string
type Lexer ¶
type Lexer struct {
Errors chan error
// contains filtered or unexported fields
}
Lexer for migo.
type NewChanStatement ¶
NewChanStatement creates and names a newly created channel.
func (*NewChanStatement) String ¶
func (s *NewChanStatement) 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.
package main
import (
"fmt"
"github.com/nickng/migo"
)
func main() {
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 Parse ¶
Parse is the entry point to the migo type parser
Example ¶
This example demonstrates the use of the Parser. The output should be exactly the same as input (but pretty printed).
package main
import (
"fmt"
"log"
"strings"
"github.com/nickng/migo"
)
func main() {
s := `def main.main(): let ch = newchan ch, 0; spawn main.sndr(ch); recv ch;
def main.sndr(ch): send ch;`
r := strings.NewReader(s)
parsed, err := migo.Parse(r)
if err != nil {
log.Fatal(err)
}
fmt.Println(parsed.String())
}
Output: def main.main(): let ch = newchan ch, 0; spawn main.sndr(ch); recv ch; def main.sndr(ch): send ch;
func (*Program) AddFunction ¶
AddFunction adds a Function to Program.
If Function already exists this does nothing.
func (*Program) CleanUp ¶
func (p *Program) CleanUp()
CleanUp removes empty functions.
Example ¶
This example demonstrates the usage of the CleanUp function to remove unwanted empty functions.
package main
import (
"fmt"
"github.com/nickng/migo"
)
func main() {
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) // Note that calling G() will be removed.
p.AddFunction(g) // Note that G() is an empty function.
p.CleanUp()
fmt.Print(p.String())
}
Output: def F(): send x;
type RecvStatement ¶
type RecvStatement struct {
Chan string
}
RecvStatement receives from Chan
func (*RecvStatement) String ¶
func (s *RecvStatement) String() string
type Scanner ¶
type Scanner struct {
// contains filtered or unexported fields
}
Scanner is a lexical scanner.
func NewScanner ¶
NewScanner returns a new instance of Scanner.
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 ¶
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 ¶
package main
import (
"fmt"
"github.com/nickng/migo"
)
func main() {
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 TauStatement ¶
type TauStatement struct{}
TauStatement is inaction.
func (*TauStatement) String ¶
func (s *TauStatement) String() string
Source Files
Directories