OpenSkillIndex← back to search
claude-codescience

Babysitter linearizability-checker

Check linearizability of concurrent data structure implementations

install
source · Clone the upstream repo
git clone https://github.com/a5c-ai/babysitter
Claude Code · Install into ~/.claude/skills/
T=$(mktemp -d) && git clone --depth=1 https://github.com/a5c-ai/babysitter "$T" && mkdir -p ~/.claude/skills && cp -r "$T/library/specializations/domains/science/computer-science/skills/linearizability-checker" ~/.claude/skills/a5c-ai-babysitter-linearizability-checker && rm -rf "$T"
manifest: library/specializations/domains/science/computer-science/skills/linearizability-checker/SKILL.md
tags
#concurrent-data#linearizability#distributed-systems#testing-framework#proof-verification#algorithm-analysis
source content

Linearizability Checker

Purpose

Provides expert guidance on verifying linearizability of concurrent data structures through testing and proof.

Capabilities

  • History linearization algorithms
  • Linearization point identification
  • Counterexample generation for violations
  • Concurrent history visualization
  • Linearizability proof templates
  • Testing framework integration

Usage Guidelines

  1. History Collection: Record concurrent operation histories
  2. Linearization: Check if history is linearizable
  3. Counterexample Analysis: Analyze non-linearizable executions
  4. Proof Construction: Build linearizability proofs
  5. Testing: Systematic testing for violations

Tools/Libraries

  • LineUp
  • Wing-Gong algorithm
  • Lincheck
  • JCStress