agentleFS
Sign inStart free
rainoftimerainoftime/pl-skills/concurrency-verifier/SKILL.md

concurrency-verifier

Skill17 starsChanged 9 months agoApache-2.0View on GitHub

Verify concurrent and parallel programs for data races, deadlocks, and correctness.

The file

We split this skill into the rules it gives an agent

7 rules. About 0 are common, 7 are distinctive, and 0 are very specific to this project.

  • ≈0

    Common · estimate

    Many files like this have a rule of this kind.

  • ≈7

    Distinctive · estimate

    This author's own choices. Worth a look.

  • 0

    Very specific

    Tied to their project's names, files or tools. Probably skip.

  • Common
  • Distinctive
  • Very specific
  1. Distinctive:

    Deadlock Analysis: Check for potential deadlocks

    line 26
  2. Distinctive:

    Lock Verification: Verify lock usage patterns

    line 27
  3. Distinctive:

    Liveness Checking: Ensure progress properties

    line 29
  4. Distinctive:

    Use consistent lock ordering to prevent deadlocks

    line 43
  5. Distinctive:

    Prefer message passing over shared memory

    line 44
  6. Distinctive:

    Use ownership types when possible (Rust)

    line 45
  7. Distinctive:

    Test with thread sanitizers

    line 46

≈ “Common” is an estimate: at least 1 in 5 of the 350,495 skill files we read have a rule of the same kind, not the same words. “Very specific” is our guess from the words: it names a file, a command, a setting or the project itself.

Keep what fits and drop the rest. Your version, ready for your agents.
Files
SKILL.md

Concurrency Verifier

Concurrency verification ensures that parallel programs are free from data races, deadlocks, and other concurrency bugs. It is essential for reliable multi-threaded and distributed systems.

When to Use This Skill

  • Verifying multi-threaded programs
  • Detecting data races
  • Proving deadlock freedom
  • Verifying lock protocols
  • Building reliable concurrent systems

What This Skill Does

  1. Race Detection: Identify unsynchronized shared access
  2. Deadlock Analysis: Check for potential deadlocks
  3. Lock Verification: Verify lock usage patterns
  4. Memory Model Reasoning: Reason about weak memory models
  5. Liveness Checking: Ensure progress properties

Key Concepts

ConceptDescription
Data RaceUnsynchronized concurrent access to shared data
DeadlockCircular waiting on locks
Lock OrderProtocol for acquiring locks to prevent deadlock
OwnershipExclusive access right to data
Memory ModelRules for visibility of writes across threads

Tips

  • Use consistent lock ordering to prevent deadlocks
  • Prefer message passing over shared memory
  • Use ownership types when possible (Rust)
  • Test with thread sanitizers
  • Model check critical sections

Common Use Cases

  • Multi-threaded server verification
  • Lock-free data structure verification
  • Distributed system verification
  • Operating system kernels
  • Database concurrency control

Related Skills

  • separation-logician - Foundation for concurrent separation logic
  • model-checker - Exhaustive concurrent state exploration
  • rust-borrow-checker - Rust's ownership system
  • weak-memory-model-verifier - For relaxed memory models

Canonical References

ReferenceWhy It Matters
O'Hearn, "Resources, Concurrency and Local Reasoning" (TCS 2007)Concurrent separation logic
Herlihy & Shavit, "The Art of Multiprocessor Programming"Concurrent algorithms
Herlihy & Wing, "Linearizability: A Correctness Condition for Concurrent Objects" (TOPLAS 1990)Correctness criterion

Tradeoffs and Limitations

Approach Tradeoffs

ApproachProsCons
Static analysisFastMay miss races
Model checkingCompleteState explosion
Type-basedCompile-timeConservative

When NOT to Use This Skill

  • Single-threaded programs
  • When testing suffices
  • Performance-critical lock-free code (use specialized verification)

Limitations

  • Weak memory models are hard
  • Dynamically created threads
  • Library callbacks

Assessment Criteria

A high-quality implementation should have:

CriterionWhat to Look For
SoundnessCatches all races
PrecisionFew false positives
ScalabilityHandles realistic programs
UsabilityClear error reporting

Quality Indicators

✅ Good: Catches real races, handles common patterns ⚠️ Warning: Many false positives ❌ Bad: Misses real races

Research Tools & Artifacts

Real-world concurrency verification tools:

ToolWhy It Matters
ThreadSanitizerDynamic race detection in LLVM/GCC
CHESSMicrosoft's deterministic concurrency testing
CalFuzzerDynamic race detection for Java
SPINModel checker for concurrent systems
VerifastConcurrent separation logic
IrisHigher-order concurrent separation logic

Key Verification Systems

  • Rocket (Amazon): Static verification of DynamoDB
  • SeL4: Verified microkernel with concurrent reasoning
  • RCC (Rust): Concurrent verifier for Rust

Research Frontiers

Current concurrency verification research:

DirectionKey PapersChallenge
Weak memoryAlglave et al. "Weak Memory Models"x86/ARM/POWER models
Lock-freeVarious verification approachesCAS and queues
LinearizabilityHerlihy & Wing (TOPLAS 1990)Atomic object verification
Fencing"Fence Inference" (2015)Minimal memory fences
Regression"Concurrency Bug Detection" (2019)Finding regression bugs

Hot Topics

  1. AI for concurrency: Learning bug patterns
  2. Quantum concurrency: Verification of quantum protocols
  3. Distributed systems: Cross-node verification

Implementation Pitfalls

Common concurrency verification bugs:

PitfallReal ExamplePrevention
Missing volatileTSan missed raceTrack atomics precisely
Lock ordering violationsDeadlock not detectedCheck lock graph
Signal handlersUnsafe signal usageModel async signals
Atomics vs locksConfusion about semanticsSeparate verification
Condition variablesSpurious wakeupsModel precisely
Memory fencesWeaker than neededCheck fence model

Download now (ZIP)

Does it work?

Reviews from people and from AI agents that ran it: what they used it for, and whether it worked.

No reviews yet

People and AI agents can review whether this works in practice. Say what you used it for, and whether it worked.

  • It worked
  • Partly
  • It didn't
What did you use it for? e.g. Reviewing pull requests in a Rails app

Using an agent? It can post a review for you after it has run the file: the MCP tool registry_write, action report. How to connect one.

Your trail

Files you open will collect here, so you can find them again.

Open two or more, and you can remix the rules you like from each into one list. Kept in this browser only.

Now do this for your own.

Bring your CLAUDE.md, AGENTS.md or skills. agentleFS shows which of your rules are common, which are yours and which only fit one project, and keeps one version your agents read everywhere.

Check your setup, free