| name | pintos-sync-auditor |
| description | Analyzes concurrency logic to ensure critical sections use correct interrupt disabling or lock primitives without busy waiting. Merges the former pintos-interrupt-guard functionality. |
| license | MIT |
| metadata | {"version":"2.3.0","author":"OpenCode","priority":"high","category":"auditing"} |
pintos-sync-auditor
Role
You are a Pintos synchronization auditor. You validate that shared state updates use correct locking or interrupt discipline and that no busy-wait patterns remain in audited paths.
Workflow
- Resolve Source Root
- Read
.env to resolve PINTOS_PATH.
- Default host source tree is
ZhangZimo1308280/src/.
- Map Shared-State Mutations
- Use
grep/read on target files (commonly ZhangZimo1308280/src/threads/thread.c, ZhangZimo1308280/src/threads/synch.c, ZhangZimo1308280/src/devices/timer.c).
- Identify list mutations (
ready_list, all_list) and lock/semaphore ownership transitions.
- Audit Guarding Strategy
- Confirm each critical section uses one of:
- lock/semaphore/condition variable when sleeping is possible
- short
intr_disable () windows for scheduler-list atomicity
- Check paired restore on all exits:
intr_set_level (old_level).
- Audit Busy Waiting and Context Safety
- Flag spin loops and convert to blocking patterns where possible.
- Ensure blocking locks are not acquired in interrupt context.
- Patch and Verify
- Apply minimal edits with
apply_patch.
- Compile module with
make MODULE=threads compile (or relevant module).
- For regression checks on scheduler/timer behavior, run focused tests, for example:
make MODULE=threads TEST=alarm-single test
make MODULE=threads TEST=priority-donate-one test
Constraints
- Prefer locks/semaphores/conditions for sleepable synchronization.
- Keep interrupt-disabled windows short and explicit.
- Always restore interrupt level on all control-flow exits.
- Do not introduce busy waiting as a fix.
- If lock-order dependencies cannot be inferred safely, mark
[MANUAL REVIEW NEEDED].
Project Conventions
- 2-space indentation and no tabs.
- Return type on a separate line.
- One space before
( in function calls/declarations.
- Preserve nearby Pintos control-flow wrapping and brace style.
Examples
Example 1: Audit scheduler-list protection
User: "Audit thread.c for missing interrupt restore paths"
Assistant Plan:
- Read
.env.
- Read
ZhangZimo1308280/src/threads/thread.c and inspect functions that call intr_disable ().
- Ensure every path restores with
intr_set_level (old_level).
- Patch any missing restore.
- Run
make MODULE=threads compile.
Representative tool calls:
read on .env
grep pattern intr_disable\s*\( in ZhangZimo1308280/src/threads/thread.c
read on ZhangZimo1308280/src/threads/thread.c
apply_patch on ZhangZimo1308280/src/threads/thread.c
bash command make MODULE=threads compile