logicprobe-concurrency
Skill5 starsChanged 8 days agoMITView on GitHub
Use when a design or plan claims concurrency safety (thread-safe, lock-free, no data race, ISR-safe) or names shared state, mutexes, atomics or interrupts. Mines the claims and routes each to dedicated verification (TSan, Helgrind, CBMC, TLA+); it does not prove concurrency safety. Doctrine: the logicprobe skill.
In this repository6 other files it gives its agents.
- AGENTS.mdAGENTS.md
- CLAUDE.mdCLAUDE.md
- logicprobe-datamodelSkill
- logicprobeSkill
- logicprobe-structureSkill
- logicprobe-umlSkill
The file
We split this skill into the rules it gives an agent
2 rules. About 0 are common, 2 are distinctive, and 0 are very specific to this project.
≈0
Common · estimate
Many files like this have a rule of this kind.
≈2
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
- Distinctive: line 44
One counterexample is enough to refute: If a race is suspected, the deliverable is the interleaving that breaks it plus the harness that …
- Distinctive: line 45
Sequential targets are out of scope: If nothing runs concurrently, say so and stop.
≈ “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.
Files
Logic Probe — Concurrency Claims
Successor:
dsh-model-everything. Its counterpart skill ismodel-everything-interleaving, which covers the same claims plus async and hands a shared location tomodel_compose_verifyinstead of routing it. Load that one when both plugins are installed; this skill stays accurate forlogicprobe_concurrency_scan.
This skill does not prove concurrency safety, and no report from it should ever be read as a proof. It mines a document, plan or code review for concurrency claims, marks them UNVERIFIED, and routes each one to the tool that can actually decide it.
The claim-verification doctrine it inherits — enumerate verifiable claims, cite file:line, read verdict and never ok — lives in the logicprobe skill. Load that one when the task is behavioural verification of a state machine rather than a judgement about concurrency claims.
When This Skill Applies
Only after confirming the target actually has concurrency requirements or behaviour — multiple threads, async tasks, interrupts, shared state, or parallel execution. If the target is purely sequential, do not invoke concurrency mining; there is nothing to mine.
| The claim | How it is treated |
| Absolute: "thread-safe", "lock-free", "no data race", "interrupt-safe", "ISR-safe" | error / UNVERIFIED unless dedicated evidence is provided |
Risk keyword: "race condition", "shared variable", "mutex", "atomic", "shared memory", "critical section", ISR, IRQ, NMI, disable_irq / enable_irq | warning — review whether the plan actually addresses it |
| Lock/unlock, alloc/free, start/stop pairing where ordering matters | routed to logicprobe model verification (A4 pair symmetry), which can decide balance inside the modelled machine |
In DSH, run the logicprobe_concurrency_scan tool. For manual review, follow references/concurrency-risk-guide.md.
Routing: What Decides Each Claim
Mining a claim is not verifying it. Hand each one to a tool that can:
| Dimension | Tool that decides it |
| Data races, lock-ordering, lock-free algorithms | ThreadSanitizer, Helgrind, or a model checker over the real code (CBMC) |
| Interrupt/ISR races, critical sections | RTOS-aware interrupt analysis, or a TLA+ model of the ISR/task interleaving |
| Protocol-level interleaving of discrete events | logicprobe_verify (S1-S8 / A1-A14) and logicprobe_compose_verify (C1/C2) |
| Hard real time: deadlines, periods, preemption | Scheduling analysis (RMA/EDF) and a timing tool — not logicprobe |
| Probability or reliability claims | PRISM/Storm, fault-tree analysis |
The full routing table, including hard-real-time, hybrid-control and execution-cost dimensions, is ../logicprobe/references/gap-routing-guide.md. logicprobe_verify reports carry the same routing as informational coverageNotes on matching models.
Rules for This Mode
- Mining, not proof. Report a concurrency claim as
UNVERIFIEDwith the routing target; never as passing. - No absolute language in the answer. "This is thread-safe" is exactly the claim being mined, not a result this skill can produce.
- One counterexample is enough to refute. If a race is suspected, the deliverable is the interleaving that breaks it plus the harness that demonstrates it (TSan/Helgrind output), not an argument.
- Sequential targets are out of scope. If nothing runs concurrently, say so and stop.
- The scanner is dsh-only.
logicprobe_concurrency_scanhas no mirror subcommand. Without it, mine the text by hand against the keyword table above and route each claim the same way. - Name the claim and its routing in words. 「QoS 1 只投递一次」plus the tool that decides it, never a bare check name. A reader who has not memorized this skill's tables learns nothing from an enumeration. The full rule is under "Writing the Answer" in the
logicprobeskill.
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
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.