liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Counting dynamically synchronizing processes
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
2016 (English)In: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, Vol. 18, no 5, 517-534 p.Article in journal (Refereed) Published
Abstract [en]

We address the problem of automatically establishing correctness for programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. The programs we consider can make use of the shared variables to count and synchronize the spawned processes. This allows them to implement intricate synchronization mechanisms, such as barriers. Automatically verifying correctness, and deadlock freedom, of such programs is beyond the capabilities of current techniques. For this purpose, we make use of counting predicates that mix counters referring to the number of processes satisfying certain properties and variables directly manipulated by the concurrent processes. We then combine existing works on counter, predicate, and constrained monotonic abstraction and build a nested counter example based refinement scheme for establishing correctness (expressed as non-reachability of configurations satisfying counting predicates formulas). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification on several programs whose correctness crucially depends on precisely capturing the number of processes synchronizing using shared variables.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2016. Vol. 18, no 5, 517-534 p.
Keyword [en]
Parameterized verification, Counting predicate, Barrier synchronization, Deadlock freedom, Multithreaded programs, Counter abstraction, Predicate abstraction, Constrained monotonic abstraction
National Category
Computer Science
Identifiers
URN: urn:nbn:se:liu:diva-124406DOI: 10.1007/s10009-015-0411-0ISI: 000382011100004OAI: oai:DiVA.org:liu-124406DiVA: diva2:898584
Note

Funding agencies: 12.04 CENIIT project

Available from: 2016-01-28 Created: 2016-01-28 Last updated: 2017-01-17

Open Access in DiVA

fulltext(742 kB)13 downloads
File information
File name FULLTEXT01.pdfFile size 742 kBChecksum SHA-512
8c30f69a6369599cf429cf53bdf64109aa0b9853caa27028c8875c241204d06b6ba33d2ccba0653cce978bf6e216bd3020abc4e2072751e6b35256762a4c18c1
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Search in DiVA

By author/editor
Ganjei, ZeinabRezine, AhmedEles, PetruPeng, Zebo
By organisation
Software and SystemsFaculty of Science & Engineering
In the same journal
International Journal on Software Tools for Technology Transfer (STTT)
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 13 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 625 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf