Exploring various implementations for goroutines support in go2pins

From LRDE

Revision as of 14:45, 30 June 2019 by Bot (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Abstract

go2pins is a tool used to interface Go programs with model checking algorithms. Through a series of transformations, a standard Go program is compiled to another behaving the same way, but exposing an interface allowing to iterate over its various states. However, go2pins currently doesn't support programs that use goroutines, Go's concurrency primitives. In this report, we present the various solutions we've assessed to implement this behaviour inside go2pins, and the problems we've had to solve along the way.