dara

Documentation

Index

• Constants
• Variables
• type CovInfo
• type CoverageEvent
• type DaraNodeStatus
• type DaraProc
• type DaraProcStatus
  • func GetDaraProcStatus(status uint32) DaraProcStatus
• type EncEvent
• type EncLogEntry
• type EncNameValuePair
• type EncodedMessage
• type Event
• type FailedPropertyEvent
• type GeneralSyscall
• type GeneralType
• type LogEntry
• type Message
• type NameValuePair
• type PropCheckEvent
  • func CreatePropCheckEvent(propertyEvents []FailedPropertyEvent, index int) PropCheckEvent
• type RoutineInfo
• type Schedule
• type TypeNum

Constants

const (
	MAP_SHARED = 0x01 // used for mmap (not defined in linux defs)
	PROT_READ  = 0x1
	PROT_WRITE = 0x2

	//The number of preallocated communication channels in shared
	//memory. This value can change in the future, for now 3 is the
	//maximum number of Processes. Invariant: dara.CHANNELS > procs. TODO
	//assert this
	// 3 is maximum because DaraProcID starts from 1.... Need to fix that
	CHANNELS = 4

	//File discriptor for shared memory. This is set in the runscript.
	DARAFD = 666

	//State of spin locks. These are used by cas operations to control
	//the execution of the insturmented runtimes
	UNLOCKED = 0
	LOCKED   = 1

	// TODO : This must be automated and not hardcoded
	// THIS SHOULD MATCH THE SIZE OF THE DaraProc struct.
	DARAPROCSIZE = 127533208

	SCHEDLEN      = 1000000000
	PROCS         = 3
	MAXGOROUTINES = 4096

	MAXLOGENTRIES   = 4096
	MAXLOGVARIABLES = 128
	VARBUFLEN       = 64
	UNSUPPORTEDVAL  = 2440
	BLOCKIDLEN      = 256
	MAXBLOCKS       = 4096
)

DARA Specific consts Constants for shared memory.

const (
	//debug levels
	DEBUG = iota
	INFO
	WARN
	FATAL
	OFF
)

const (
	BOOL_STRING   = "bool"
	INT_STRING    = "int"
	FLOAT_STRING  = "float"
	STRING_STRING = "string"
)

loggging consts

const (
	DSYS_READ = iota
	DSYS_WRITE
	DSYS_OPEN
	DSYS_CLOSE
	DSYS_STAT
	DSYS_FSTAT
	DSYS_LSTAT
	DSYS_LSEEK
	DSYS_PREAD64
	DSYS_PWRITE64
	DSYS_GETPAGESIZE
	DSYS_EXECUTABLE
	DSYS_GETPID
	DSYS_GETPPID
	DSYS_GETWD
	DSYS_READDIR
	DSYS_READDIRNAMES
	DSYS_WAIT4
	DSYS_KILL
	DSYS_GETUID
	DSYS_GETEUID
	DSYS_GETGID
	DSYS_GETEGID
	DSYS_GETGROUPS
	DSYS_EXIT
	DSYS_RENAME
	DSYS_TRUNCATE
	DSYS_UNLINK
	DSYS_RMDIR
	DSYS_LINK
	DSYS_SYMLINK
	DSYS_PIPE2
	DSYS_MKDIR
	DSYS_CHDIR
	DSYS_UNSETENV
	DSYS_GETENV
	DSYS_SETENV
	DSYS_CLEARENV
	DSYS_ENVIRON
	DSYS_TIMENOW
	DSYS_READLINK
	DSYS_CHMOD
	DSYS_FCHMOD
	DSYS_CHOWN
	DSYS_LCHOWN
	DSYS_FCHOWN
	DSYS_FTRUNCATE
	DSYS_FSYNC
	DSYS_UTIMES
	DSYS_FCHDIR
	DSYS_SETDEADLINE
	DSYS_SETREADDEADLINE
	DSYS_SETWRITEDEADLINE
	DSYS_NET_READ
	DSYS_NET_WRITE
	DSYS_NET_CLOSE
	DSYS_NET_SETDEADLINE
	DSYS_NET_SETREADDEADLINE
	DSYS_NET_SETWRITEDEADLINE
	DSYS_NET_SETREADBUFFER
	DSYS_NET_SETWRITEBUFFER
	DSYS_SOCKET
	DSYS_LISTEN_TCP
	DSYS_SLEEP
	MUX_LOCK
	MUX_UNLOCK
	WG_ADD
	WG_WAIT
	CTX_DONE
	CTX_CANCEL
	DSYS_TIMER
)

Dara Syscall Numbers. These are the numbers used for identification of syscalls by the scheduler.

const (
	LOG_EVENT = iota
	SYSCALL_EVENT
	SEND_EVENT
	REC_EVENT
	SCHED_EVENT
	INIT_EVENT
	END_EVENT
	THREAD_EVENT
	CRASH_EVENT
	DELETEVAR_EVENT
	TIMER_EVENT
)

Event Types

const (
	// THe global scheduler has asked us the local scheduler
	// to record events of interest and report them to the global scheduler
	RECORD DaraNodeStatus = -3
	INIT                  = -1
	// The local scheduler has finished its execution
	FINISH = -100
	// The global scheduler has told the local scheduler to kill its execution.
	KILL = -4
	// The local scheduler needs to do polling on the net. It can't do anything else for now :/
	NET_BLOCK = -6
	// The local scheduler has woken up from a network block. This value notifies
	// the global scheduler that it wants the lock back
	NET_WAKEUP = -7
	// The global scheduler has specified the next GoRoutine that must be executed
	// This value is only used during replay and explore
	ROUTINE_SCHEDULE = -5
)

Variables

var GStatusStrings = [...]string{
	// contains filtered or unexported fields
}

array of status to string from runtime/proc.go

Types

type CovInfo

type CovInfo struct {
	BlockID [BLOCKIDLEN]byte
	Count   uint64
}

type CoverageEvent

type CoverageEvent struct {
	CoverageInfo     map[string]uint64
	SnapshotCoverage float64
	TotalCoverage    float64
	EventIndex       int
}

type DaraNodeStatus

type DaraNodeStatus int

Status is used to control between Global and Local Schedulers

type DaraProc

type DaraProc struct {

	//Lock is used to control the execution of a process. A process
	//which is running but Not scheduled will spin on this lock using
	//checkandset operations If the lock is held The owner can modify
	//the state of the DaraProc
	Lock uint32

	//SyscallLock is used to control the reporting of the syscalls.
	SyscallLock uint32

	//PID is the Linux Process ID. Since we are limited to GOMAXPROCS=1
	//there is only 1 system thread/process ID.
	PID uint64

	//Run is a deprecated var with multiple purposes. Procs set their
	//Run to -1 when they Are done running (in replay mode) to let the
	//scheduler know they are done. The global scheduler sets this
	//value to 2 to let the runtime know its replay, and 3 for record
	//1 is used to denote the first event, and 0 indicates this
	//variable has not been initialized Originally Run was intended to
	//report the id of the goroutine that was executed, but that was
	//not always the same so the program counter  was needed, now
	//RunningRoutine is used to report this. The global scheduler sets
	// this to -4 to inform the local schedulers that replay is ended
	Run int
	// Syscall number at which the running routine is blocked on. -1 means that
	// there is no syscall on which the daraproc is blocked
	Syscall int
	//RunningRoutine is the goroutine scheduled, running, or ran, for
	//any single replayed event in a schedule. In Record, the
	//executed goroutine is reported via this variable, in Replay the
	//global scheduler tells the runtime which routine to run with
	//RunningRoutine
	RunningRoutine RoutineInfo
	//Routines is the full set of goroutines a process is allowed to
	//run. The total number is allocated upfront so that shared memory
	//does not need to be resized dynamically. After each iteration
	//of scheduling runtimes update the states of all their routines
	//via this structure
	Routines [MAXGOROUTINES]RoutineInfo
	//TODO document
	Epoch         int
	LogIndex      int
	Log           [MAXLOGENTRIES]EncEvent
	CoverageIndex int
	Coverage      [MAXBLOCKS]CovInfo
}

DaraProc is used to communicate control and data information between a single instrumented go runtime and the global scheduler. One of these structures is mapped into shared memory for each process that is launched during an execution. If there are more runtimes active Than DaraProcs the additional runtimes will not be controlled by the global scheduler, or Segfault immediately

type DaraProcStatus

type DaraProcStatus uint32

const (
	Idle             DaraProcStatus = iota // 0
	Runnable                               // 1
	Running                                // 2
	Syscall                                // 3
	Waiting                                // 4
	Moribound_Unused                       // 5
	Dead                                   // 6
	Enqueue_Unused                         // 7
	Copystack                              // 8
	Scan             DaraProcStatus = 0x1000
	ScanRunnable                    = Scan + Runnable // 0x1001
	ScanRunning                     = Scan + Running  // 0x1002
	ScanSyscall                     = Scan + Syscall  // 0x1003
	ScanWaiting                     = Scan + Waiting  // 0x1004
)

The numbering has to match the Goroutine states from runtime/proc.go

func GetDaraProcStatus

func GetDaraProcStatus(status uint32) DaraProcStatus

type EncEvent

type EncEvent struct {
	Type        int
	P           int
	G           RoutineInfo
	Epoch       int
	ELE         EncLogEntry
	SyscallInfo GeneralSyscall
	EM          EncodedMessage
}

type EncLogEntry

type EncLogEntry struct {
	Length int
	LogID  [VARBUFLEN]byte
	Vars   [MAXLOGVARIABLES]EncNameValuePair
}

type EncNameValuePair

type EncNameValuePair struct {
	VarName [VARBUFLEN]byte
	Value   [VARBUFLEN]byte
	Type    [VARBUFLEN]byte
}

type EncodedMessage

type EncodedMessage struct {
	Body [VARBUFLEN]byte
}

TODO fill out this structure

type Event

type Event struct {
	Type        int
	P           int
	G           RoutineInfo
	Epoch       int
	LE          LogEntry
	SyscallInfo GeneralSyscall
	Msg         Message
}

type FailedPropertyEvent

type FailedPropertyEvent struct {
	Name    string
	Context map[string]interface{}
}

type GeneralSyscall

type GeneralSyscall struct {
	SyscallNum int
	NumArgs    int
	NumRets    int
	Args       [10]GeneralType
	Rets       [10]GeneralType
}

type GeneralType

type GeneralType struct {
	Type        TypeNum
	Integer     int
	Bool        bool
	Float       float32
	Integer64   int64
	String      [256]byte
	Unsupported rune
}

type LogEntry

type LogEntry struct {
	LogID string
	Vars  []NameValuePair
}

type Message

type Message struct {
	Body string
}

type NameValuePair

type NameValuePair struct {
	VarName string
	Value   interface{}
	Type    string
}

type PropCheckEvent

type PropCheckEvent struct {
	PropFailures []FailedPropertyEvent
	EventIndex   int
}

func CreatePropCheckEvent

func CreatePropCheckEvent(propertyEvents []FailedPropertyEvent, index int) PropCheckEvent

type RoutineInfo

type RoutineInfo struct {
	//Set to one of the statuses in the constant block above
	Status uint32
	//Goroutine id as set by the runtime. This is sometimes usefull
	//for detecting which routine is which, but it is not always the
	//same between runs. However 1 is allways main, while 2 is a
	//finalizer, and 3 is a garbage collection invocator.
	Gid int
	//Program counter that this goroutine was launched from
	Gpc uintptr
	//A count of how many other goroutines were launched on the same
	//pc prior to this goroutine. (Gpc,Routinecount) is a unique id
	//for a goroutine on a given processor.
	RoutineCount int
	//A textual description of the function this goroutine was forked
	//from.In the future it can be removed.
	FuncInfo [64]byte
}

RoutineInfo contains data specific to a single goroutine

type Schedule

type Schedule struct {
	LogEvents  []Event
	CovEvents  []CoverageEvent
	PropEvents []PropCheckEvent
}

Type which encapsulates a single schedule

type TypeNum

type TypeNum int

const (
	INTEGER TypeNum = iota
	INTEGER64
	BOOL
	FLOAT
	STRING
	ARRAY
	ERROR
	POINTER
	FILE
	FILEINFO
	CONNECTION
	TIME
	PROCESS
	SIGNAL
	CONTEXT
	SOCKADDR
)