Exploring various implementations for goroutines support in go2pins

From LRDE

The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

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.