migo

package module
v3.0.6 Latest Latest
Warning

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

 Go to latest Published: Dec 6, 2022 License: Apache-2.0 Imports: 8 Imported by: 1

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

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 NamedVar
}

NewMem creates a new memory or variable reference.

func (*NewMem) String 

func (s *NewMem) String() string

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 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
	Pos  token.Position
}

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
	Pos  token.Position
}

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

Source Files

View all 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.

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.