Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
    • Switch to GitLab Next
  • Sign in / Register
CPAchecker
CPAchecker
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 313
    • Issues 313
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 11
    • Merge requests 11
  • Requirements
    • Requirements
    • List
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Operations
    • Operations
    • Incidents
    • Environments
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • CI/CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • SoSy-Lab
  • Software
  • CPAcheckerCPAchecker
  • Issues
  • #464

Closed
Open
Created Sep 26, 2018 by Karlheinz Friedberger@kfriedbergerMaintainer

ThreadingCPA: support PredicateAnalysis

Currently it is not possible to use PredicateCPA with ThreadingCPA to verify multi-threaded tasks. This issue is just a documentation about the things to do. This issue is not related to ParallelBAM (conceptually we cannot combine BAM with ThreadingCPA).

PredicateCPA has some internal dependencies and assumptions that fail with multi-threaded tasks. The following is an initial (incomplete) list:

  • one program location per abstract state. ThreadingCPA has more locations per abstract state.
  • one program location per predicate in the precision. Might even work, if the abstraction uses predicates if any location matches.
  • determine most efficient block size. SBE should work, LBE might be a problem due to heavy branching and merging. The block operator does not consider multiple locations per abstract state. Best solution so far: use existing block operator and compute abstractions whenever any of the available locations triggers a block-end.
  • at most two outgoing branches in counterexamples. This seems to only print a warning, maybe not a problem.

We need to take a look at them, and then check whether and how we can weaken them.

As an initial step, BMC could be extended to support concurrent programs. This could be used to enable counterexample checking for our current analyses of concurrent programs.

Edited Nov 04, 2020 by Karlheinz Friedberger
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking