View in EDS

Model checking of concurrent programs with static analysis of field accesses.

Saved in:
Bibliographic Details
Title: Model checking of concurrent programs with static analysis of field accesses.
Authors: Parízek, Pavel1 parizek@d3s.mff.cuni.cz, Lhoták, Ondřej2 olhotak@uwaterloo.ca
Source: Science of Computer Programming. Feb2015 Part 4, Vol. 98, p735-763. 29p.
Subjects: Concurrent error detection, Threads (Computer programs), Java programming language, Computer software execution, Information technology, Data reduction
Abstract: Systematic exploration of all possible thread interleavings is a popular approach to detect errors in multi-threaded programs. A common strategy is to use a partial order reduction technique and perform a non-deterministic thread scheduling choice only when the next instruction to be executed may possibly read or modify the global state. However, some verification frameworks and software model checkers, including Java Pathfinder (JPF), construct the program state space on-the-fly during traversal. The partial order reduction technique built into such a tool can use only the information available in the current state to determine whether the execution of a given instruction is globally-relevant. For example, the reduction technique has to make a thread choice at every field access on a heap object reachable from multiple threads, even in the case of fields that are really accessed only by a single thread during program execution, because it does not have any information about what may happen in the future after a particular state. These conservative decisions cause many redundant thread choices. We propose static analyses that identify globally-relevant field accesses more precisely. For each program state, the analyses give information about field accesses that may occur in the future after the given state. The state space traversal algorithm can use this information to soundly avoid creating unnecessary thread choices, and thus to reduce the number of thread interleavings that must be explored to cover all distinct behaviors of the given program. We implemented the proposed analyses using WALA and integrated them with JPF. Results of experiments on several Java programs show that the static analyses greatly improve the performance and scalability of JPF. In particular, it is now possible to check more complex programs than before in reasonable time. [ABSTRACT FROM AUTHOR]
Copyright of Science of Computer Programming is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 99791530
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Model checking of concurrent programs with static analysis of field accesses.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Parízek%2C+Pavel%22">Parízek, Pavel</searchLink><relatesTo>1</relatesTo><i> parizek@d3s.mff.cuni.cz</i><br /><searchLink fieldCode="AR" term="%22Lhoták%2C+Ondřej%22">Lhoták, Ondřej</searchLink><relatesTo>2</relatesTo><i> olhotak@uwaterloo.ca</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Science+of+Computer+Programming%22">Science of Computer Programming</searchLink>. Feb2015 Part 4, Vol. 98, p735-763. 29p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Concurrent+error+detection%22">Concurrent error detection</searchLink><br /><searchLink fieldCode="DE" term="%22Threads+%28Computer+programs%29%22">Threads (Computer programs)</searchLink><br /><searchLink fieldCode="DE" term="%22Java+programming+language%22">Java programming language</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+software+execution%22">Computer software execution</searchLink><br /><searchLink fieldCode="DE" term="%22Information+technology%22">Information technology</searchLink><br /><searchLink fieldCode="DE" term="%22Data+reduction%22">Data reduction</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: Systematic exploration of all possible thread interleavings is a popular approach to detect errors in multi-threaded programs. A common strategy is to use a partial order reduction technique and perform a non-deterministic thread scheduling choice only when the next instruction to be executed may possibly read or modify the global state. However, some verification frameworks and software model checkers, including Java Pathfinder (JPF), construct the program state space on-the-fly during traversal. The partial order reduction technique built into such a tool can use only the information available in the current state to determine whether the execution of a given instruction is globally-relevant. For example, the reduction technique has to make a thread choice at every field access on a heap object reachable from multiple threads, even in the case of fields that are really accessed only by a single thread during program execution, because it does not have any information about what may happen in the future after a particular state. These conservative decisions cause many redundant thread choices. We propose static analyses that identify globally-relevant field accesses more precisely. For each program state, the analyses give information about field accesses that may occur in the future after the given state. The state space traversal algorithm can use this information to soundly avoid creating unnecessary thread choices, and thus to reduce the number of thread interleavings that must be explored to cover all distinct behaviors of the given program. We implemented the proposed analyses using WALA and integrated them with JPF. Results of experiments on several Java programs show that the static analyses greatly improve the performance and scalability of JPF. In particular, it is now possible to check more complex programs than before in reasonable time. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Science of Computer Programming is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=99791530
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1016/j.scico.2014.10.008
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 29
        StartPage: 735
    Subjects:
      – SubjectFull: Concurrent error detection
        Type: general
      – SubjectFull: Threads (Computer programs)
        Type: general
      – SubjectFull: Java programming language
        Type: general
      – SubjectFull: Computer software execution
        Type: general
      – SubjectFull: Information technology
        Type: general
      – SubjectFull: Data reduction
        Type: general
    Titles:
      – TitleFull: Model checking of concurrent programs with static analysis of field accesses.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Parízek, Pavel
      – PersonEntity:
          Name:
            NameFull: Lhoták, Ondřej
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 04
              M: 02
              Text: Feb2015 Part 4
              Type: published
              Y: 2015
          Identifiers:
            – Type: issn-print
              Value: 01676423
          Numbering:
            – Type: volume
              Value: 98
          Titles:
            – TitleFull: Science of Computer Programming
              Type: main
ResultId 1