Skip to main content
Top
Published in: International Journal on Software Tools for Technology Transfer 1/2023

06-01-2023 | General

Go2Pins: a framework for the LTL verification of Go programs (extended version)

Authors: Alexandre Kirszenberg, Antoine Martin, Hugo Moreau, Etienne Renault

Published in: International Journal on Software Tools for Technology Transfer | Issue 1/2023

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We introduce Go2Pins, a tool that takes a program written in Go and links it with two model checkers: LTSMin (Kant et al. Ltsmin: high-performance language-independent model checking. In: TACAS’15, pp. 692–707, 2015) and Spot (Duret-Lutz et al. Spot 2.0-a framework for LTL and \({\omega }\) automata manipulation. In: ATVA’16, vol. 9938 of LNCS, pp. 1294, 122–129, 2016) . Go2Pins is an effort to promote the integration of both formal verification and testing inside industrial-size projects. With this goal in mind, we introduce black-box transitions, an efficient and scalable technique for handling the Go runtime. This approach, inspired by hardware verification techniques, allows easy, automatic and efficient abstractions. Go2Pins also handles basic concurrent programs through the use of a dedicated scheduler. Moreover, in order to efficiently handle recursive programs, we introduce PSL\(_{\textsc {Rec}}\), a formalism that augments PSL without changing the complexity of the underlying verification process. In this paper we demonstrate the usage of Go2Pins over benchmarks inspired by industrial problems and a set of LTL formulae. Even if Go2Pins is still at the early stages of development, our results are promising and show the benefits of using black-box transitions. This paper also shows how Go2Pins is able to work efficiently on two bugs coming from industrial problems Kubernetes and Trillian.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
Note that in the particular context of CSP, validity can also be checked using refinement.
 
2
In compiler realm, a difference is made between compilers that usually produce a directly usable artifact, whereas transpilers produce another form of source code.
 
3
Model checkers represent the model as a Kripke structure. These two functions are enough to provide a Kripke view of a Go program.
 
4
This is achieved by building one last extra function: G2PMain (see line 42). This function takes a state vector as a parameter and returns an initialized state vector during the first call. Then, this function dispatches the processing of the computation to the function under execution.
 
5
In practice, this state represents the increment of the program counter.
 
6
Here we merge LabelCounter and FunctionCounter for the sake of clarity.
 
7
or structural typing
 
8
Note that Go2Pins handles the same way, nested structures.
 
9
Virtual dispatches are calls to function Say().
 
10
The runtime of programming language is traditionally provided as a dynamic library.
 
11
Notice that this technique is only possible since Go2Pins is developed in Go and produces Go files.
 
13
Another restriction concerns the use of the LTL Next operator. Indeed, if the black-boxed function has multiple modification of one variable, only the later one will be visible.
 
14
Note that only the Spot backend supports PSL.
 
18
This approach is valid at least until we reach the core translation
 
19
Details of our benchmark and how to reproduce it are available at https://​www.​lre.​epita.​fr/​~renault/​benchs/​SPIN-2021/​results.​html
 
20
In our benchmarks multiples programs have the same number of line of code (LOC). A series is defined as all computations, i.e., one per formula, w.r.t. a specific LOC.
 
21
We also plan to translate the Promela database http://​www.​albertolluch.​com/​research/​promelamodels to Go in order to compare with other verification tools
 
22
Although PSL\(_{\textsc {Rec}}\) itself supports PSL syntax, only pure LTL formulas were used for this evaluation since LTSMin’s default translation backend only supports LTL syntax.
 
24
An adaptation of this program w.r.t the constraints of Gomela
 
25
This is handled by some omitted code line 34
 
Literature
1.
go back to reference Baranova, Z., Barnat, J., Kejstova, K., Kucera, T., Lauko, H., Mrazek, J., Rockai, P., Still, V.: Model checking of C and C++ with DIVINE 4. In ATVA’17, vol. 10482 of LNCS, pp. 201–207. Springer, (2017) Baranova, Z., Barnat, J., Kejstova, K., Kucera, T., Lauko, H., Mrazek, J., Rockai, P., Still, V.: Model checking of C and C++ with DIVINE 4. In ATVA’17, vol. 10482 of LNCS, pp. 201–207. Springer, (2017)
2.
go back to reference Berthelot, G.: Checking properties of nets using transformation. In Applications and Theory in Petri Nets, vol. 222 of LNCS, pp. 19–40. Springer, (1985) Berthelot, G.: Checking properties of nets using transformation. In Applications and Theory in Petri Nets, vol. 222 of LNCS, pp. 19–40. Springer, (1985)
3.
go back to reference Berthomieu, B., Le Botlan, D., Dal Zilio, S.: Counting Petri net markings from reduction equations. Int. J. Softw. Tools Technol. Transf. (2019) Berthomieu, B., Le Botlan, D., Dal Zilio, S.: Counting Petri net markings from reduction equations. Int. J. Softw. Tools Technol. Transf. (2019)
4.
go back to reference Blahoudek, F., Duret-Lutz, A., Rujbr, V., Strejček, J.: On refinement of Büchi automata for explicit model checking. In SPIN’15, vol. 9232 of LNCS, pp. 66–83. Springer, Aug. (2015) Blahoudek, F., Duret-Lutz, A., Rujbr, V., Strejček, J.: On refinement of Büchi automata for explicit model checking. In SPIN’15, vol. 9232 of LNCS, pp. 66–83. Springer, Aug. (2015)
5.
go back to reference Bloemen, V., van de Pol, J.: Multi-core scc-based ltl model checking. In HVC’16, vol. 10028 of LNCS, pp. 18–33. Springer, Nov. (2016) Bloemen, V., van de Pol, J.: Multi-core scc-based ltl model checking. In HVC’16, vol. 10028 of LNCS, pp. 18–33. Springer, Nov. (2016)
6.
go back to reference Dekker, J., Vaandrager, F., Smetsers, R.: Generating a google go framework from an uppaal model. Master’s thesis. Radboud University (2014) Dekker, J., Vaandrager, F., Smetsers, R.: Generating a google go framework from an uppaal model. Master’s thesis. Radboud University (2014)
7.
go back to reference Dilley, N., Lange, J.: An empirical study of messaging passing concurrency in go projects. In 2019 IEEE 26th International Conference on Software Analysis, Evolution and Reengineering (SANER’19), pp. 377–387, (2019) Dilley, N., Lange, J.: An empirical study of messaging passing concurrency in go projects. In 2019 IEEE 26th International Conference on Software Analysis, Evolution and Reengineering (SANER’19), pp. 377–387, (2019)
9.
go back to reference Dilley,N., Lange, J.: Automated verification of go programs via bounded model checking. In 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 1016–1027, (2021) Dilley,N., Lange, J.: Automated verification of go programs via bounded model checking. In 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 1016–1027, (2021)
10.
go back to reference Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 — a framework for LTL and \(\omega \)-automata manipulation. In ATVA’16, vol. 9938 of LNCS, pp. 122–129. Springer, Oct. (2016) Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 — a framework for LTL and \(\omega \)-automata manipulation. In ATVA’16, vol. 9938 of LNCS, pp. 122–129. Springer, Oct. (2016)
11.
go back to reference Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Series on Integrated Circuits and Systems (2006) Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Series on Integrated Circuits and Systems (2006)
12.
go back to reference Evangelista, S., Laarman, A., Petrucci, L., van de Pol, J.: Improved multi-core nested depth-first search. In ATVA’12, vol. 7561 of LNCS, pp. 269–283. Springer, (2012) Evangelista, S., Laarman, A., Petrucci, L., van de Pol, J.: Improved multi-core nested depth-first search. In ATVA’12, vol. 7561 of LNCS, pp. 269–283. Springer, (2012)
21.
go back to reference Giunti, M.: Gopi: Compiling linear and static channels in go. In Coordination Models and Languages, pp. 137–152, (2020) Springer Giunti, M.: Gopi: Compiling linear and static channels in go. In Coordination Models and Languages, pp. 137–152, (2020) Springer
22.
go back to reference Godefroid, P.: Between testing and verification: Dynamic software model checking. In DSSE’16 45, pp. 99–116 (2016) Godefroid, P.: Between testing and verification: Dynamic software model checking. In DSSE’16 45, pp. 99–116 (2016)
24.
go back to reference Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall Inc, USA (1985)MATH Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall Inc, USA (1985)MATH
25.
go back to reference Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley (2003) Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley (2003)
26.
go back to reference Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: Ltsmin: high-performance language-independent model checking. In TACAS’15, pp. 692–707, April (2015) Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: Ltsmin: high-performance language-independent model checking. In TACAS’15, pp. 692–707, April (2015)
27.
go back to reference Kirszenberg,A., Martin, A., Moreau, H., Renault, E.: Go2Pins: a framework for the LTL verification of Go programs. In SPIN’21, vol. 12864 of LNCS, pp. 140–156, May (2021) Springer Kirszenberg,A., Martin, A., Moreau, H., Renault, E.: Go2Pins: a framework for the LTL verification of Go programs. In SPIN’21, vol. 12864 of LNCS, pp. 140–156, May (2021) Springer
28.
go back to reference Laarman,A.: Stubborn transaction reduction. In NFM, vol. 10811 of LNCS, pp. 280–298. Springer, (2018) Laarman,A.: Stubborn transaction reduction. In NFM, vol. 10811 of LNCS, pp. 280–298. Springer, (2018)
29.
go back to reference Laarman, A., Pater, E., van de Pol, J., Hansen, H.: Guard-based partial-order reduction. Int. J. Softw. Tools Technol. Transf. 1–22, (2014) Laarman, A., Pater, E., van de Pol, J., Hansen, H.: Guard-based partial-order reduction. Int. J. Softw. Tools Technol. Transf. 1–22, (2014)
30.
go back to reference Lange,J., Ng, N., Toninho, B., Yoshida, N.: Fencing off Go: Liveness and Safety for Channel-based Programming. In POPL’17, pp. 748–761. ACM, (2017) Lange,J., Ng, N., Toninho, B., Yoshida, N.: Fencing off Go: Liveness and Safety for Channel-based Programming. In POPL’17, pp. 748–761. ACM, (2017)
31.
go back to reference Lange,J., Ng, N., Toninho, B., Yoshida, N.: A static verification framework for message passing in Go using behavioural Types. In CSE’18, pp. 1137–1148. ACM, (2018) Lange,J., Ng, N., Toninho, B., Yoshida, N.: A static verification framework for message passing in Go using behavioural Types. In CSE’18, pp. 1137–1148. ACM, (2018)
33.
go back to reference Liu, Z., Zhu, S., Qin, B., Chen, H., Song, L.: Automatically detecting and fixing concurrency bugs in go software systems. In: International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) 11, pp. 2227–2240 (2016) Liu, Z., Zhu, S., Qin, B., Chen, H., Song, L.: Automatically detecting and fixing concurrency bugs in go software systems. In: International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) 11, pp. 2227–2240 (2016)
34.
go back to reference Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In PODC’90, pp. 377–410, (1990) ACM Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In PODC’90, pp. 377–410, (1990) ACM
35.
go back to reference Ng, N., Yoshida, N.: Static deadlock detection for concurrent go by global session graph synthesis. In CCC’16, pp. 174–184. ACM, (2016) Ng, N., Yoshida, N.: Static deadlock detection for concurrent go by global session graph synthesis. In CCC’16, pp. 174–184. ACM, (2016)
36.
go back to reference Peled, D.: Combining partial order reductions with on-the-fly model-checking. In CAV’94, vol. 818 of LNCS, pp. 377–390. Springer, (1994) Peled, D.: Combining partial order reductions with on-the-fly model-checking. In CAV’94, vol. 818 of LNCS, pp. 377–390. Springer, (1994)
37.
go back to reference Ray, B., Posnett, D., Filkov, V., Devanbu, P.: A large scale study of programming languages and code quality in github. In SIGSOFT’14, pp. 155–165, (2014) Ray, B., Posnett, D., Filkov, V., Devanbu, P.: A large scale study of programming languages and code quality in github. In SIGSOFT’14, pp. 155–165, (2014)
39.
go back to reference Tu, T., Liu, X., Song, L., Zhang, Y.: Understanding real-world concurrency bugs in go. In ASPLOS’19, pp. 865–878, (2019) Tu, T., Liu, X., Song, L., Zhang, Y.: Understanding real-world concurrency bugs in go. In ASPLOS’19, pp. 865–878, (2019)
40.
go back to reference Valmari, A.: Stubborn sets for reduced state space generation. In ICATPN’91, vol. 618 of LNCS, pp. 491–515, (1991) Springer Valmari, A.: Stubborn sets for reduced state space generation. In ICATPN’91, vol. 618 of LNCS, pp. 491–515, (1991) Springer
41.
go back to reference Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model Checking Programs. In ASE’03 10, pp. 203–232 (2018) Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model Checking Programs. In ASE’03 10, pp. 203–232 (2018)
42.
go back to reference Yuan, T., Li, G., Lu, J., Liu, C., Li, L., Xue, J.: Gobench: A benchmark suite of real-world go concurrency bugs. In 2021 IEEE/ACM International Symposium on Code Generation and Optimization (CGO), pp. 187–199, (2021) Yuan, T., Li, G., Lu, J., Liu, C., Li, L., Xue, J.: Gobench: A benchmark suite of real-world go concurrency bugs. In 2021 IEEE/ACM International Symposium on Code Generation and Optimization (CGO), pp. 187–199, (2021)
43.
go back to reference Zaks, A., Joshi, R.: Verifying Multi-threaded C Programs with SPIN. In SPIN’08, pp. 94–107, (2008) Zaks, A., Joshi, R.: Verifying Multi-threaded C Programs with SPIN. In SPIN’08, pp. 94–107, (2008)
44.
go back to reference Zhong,C., Zhao, Q., Liu, X.: Bingo: Pinpointing concurrency bugs in go via binary analysis, (2022) Zhong,C., Zhao, Q., Liu, X.: Bingo: Pinpointing concurrency bugs in go via binary analysis, (2022)
Metadata
Title
Go2Pins: a framework for the LTL verification of Go programs (extended version)
Authors
Alexandre Kirszenberg
Antoine Martin
Hugo Moreau
Etienne Renault
Publication date
06-01-2023
Publisher
Springer Berlin Heidelberg
Published in
International Journal on Software Tools for Technology Transfer / Issue 1/2023
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-022-00692-w

Other articles of this Issue 1/2023

International Journal on Software Tools for Technology Transfer 1/2023 Go to the issue

Premium Partner