Skip to main content
Erschienen 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)

verfasst von: Alexandre Kirszenberg, Antoine Martin, Hugo Moreau, Etienne Renault

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 1/2023

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Fußnoten
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
 
Literatur
1.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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)
32.
33.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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)
Metadaten
Titel
Go2Pins: a framework for the LTL verification of Go programs (extended version)
verfasst von
Alexandre Kirszenberg
Antoine Martin
Hugo Moreau
Etienne Renault
Publikationsdatum
06.01.2023
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 1/2023
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-022-00692-w

Weitere Artikel der Ausgabe 1/2023

International Journal on Software Tools for Technology Transfer 1/2023 Zur Ausgabe

Premium Partner