AtomiS: Data-Centric Synchronization Made Practical
summary
AtomiS implements a Java data-centric synchronization model that requires only qualified types on interfaces and fields, then runs a static analysis to infer per-method atomicity variants and generates code for each valid variant; a lock-injection pass (lock-based, M exclusion or RW locks) enforces absence of races, atomicity violations and deadlocks. Benchmarks show fewer annotations than Atomic Sets, compilation averages ~5s (under 20s), runtime is competitive with lock-based Java; type-soundness is mechanized in Coq while lock-inference soundness is in progress.
AI-written summary · about
chapters (14)
- 0:00AtomiS introduction
- 1:05Data-centric sync
- 2:09Type qualifiers approach
- 3:34Units of work
- 6:29Units work semantics
- 7:53Composition of units
- 8:57Type params for atomicity
- 10:45Concurrent list impl
- 11:30Compilation pipeline
- 12:55Formalization soundness
- 13:58Evaluation Java Collections
- 15:01Performance vs Java API
- 16:29Key features
- 17:39Q&A
related talks
16mFast Atomicity Monitoring
52mNonblocking algorithms/ CAS/Atomics
01h 22mBeyond Sequential Consistency - Leveraging Atomics for Fun & Profit
01h 08mSimplifying Concurrent Programming via Synchronization Synthesis
43mWhen Atomics Lose - Architecture‑Dependent Performance of C++ Synchronization
17mInferring Likely Counting-related Atomicity Program Properties for Persistent...
01h 03mUsing weakly ordered C++ atomics correctly
31mSynthesizing fine-grained synchronization protocols for implicit monitors