KAIST Concurrency and Parallelism
We design and verify innovative concurrent and parallel systems.
We are currently seeking enthusiastic students at all academic levels who are interested in designing and verifying concurrent and parallel systems. If this interests you, please review these instructions and then contact Jeehoon as soon as possible.
Projects
In the era of big data, artificial intelligence, and the Internet of Things, the demand for computing resources is rapidly increasing. However, these resources are becoming scarce due to the slowing of Dennard scaling and Moore’s law. The most viable solution to address this shortage is to massively parallelize computing resources, helping to offset the impact of this slowdown.
Our objective is to design, implement, and verify such massively parallel systems. These systems range from microarchitectures to programming languages and algorithms, aiming to significantly enhance performance and reduce power consumption compared to conventional systems.
Our approach to achieving this goal involves three main strategies: (1) gaining a holistic understanding of the entire computer systems; (2) designing abstraction layers that harness the intrinsic parallelism of workloads while simultaneously offering an easy programming environment; and (3) formally verifying these abstraction layers to ensure their safe and confident use by users.
Specifically, our focus is on the design and verification of concurrent and parallel systems:
-
Designing concurrent and parallel systems: Developing efficient yet safe concurrent software and hardware is challenging. Efficient systems must support concurrent accesses by multiple threads or components, which complicates safety considerations.
Therefore, we are developing design principles for managing concurrent accesses and creating practical concurrent systems based on these principles. Our current projects include:
- AI systems (compilers and runtimes), optimized for NPUs in partnership with FuriosaAI
- Hardware design languages, implementing CPUs, NPUs, TCP/IP engine
- Concurrent garbage collection, achieving high throughput and low latency
- High-performance storage systems, based on robust design principles like Memento and next-genereation devices like Samsung CMM-H
- Quantum programming languages, capturing the essence of quantum computation
-
Verifying concurrent and parallel systems: Ensuring the safety of concurrent software and hardware through testing alone is challenging due to the inherent non-determinism from scheduling, optimization, and other factors.
Thus, we are developing verification techniques to prove the correctness of concurrent systems and verify real-world systems like operating systems, database systems, or cache coherence protocols. This helps us explore whether verification is more cost-effective than testing for concurrent systems. Our verification projects include:
- Operating systems in Rust
- Concurrent data structures and garbage collection
- Hardware designs
Publications
-
(OOPSLA 2024)
Quantum Probabilistic Model Checking for Time-bounded Properties.
Seungmin Jeon, Kyeongmin Cho, Chan Gu Kang, Janggun Lee, Hakjoo Oh, Jeehoon Kang.
Object-oriented Programming, Systems, Languages, and Applications.
[paper: doi, local]
-
(2024)
Taming shared mutable states of operating systems in Rust.
Jaemin Hong, Sunghwan Shim, Sanguk Park, Taewoo Kim, Jungwoo Kim, Junsoo Lee, Sukyoung Ryu, Jeehoon Kang.
Science of Computer Programming.
[paper: doi] [artifact: rv6]
-
(SPAA 2024)
Expediting Hazard Pointers with Bounded RCU Critical Sections.
Jeonghyeon Kim, Jaehwang Jung, Jeehoon Kang.
ACM Symposium on Parallelism in Algorithms and Architectures (Best Paper Award).
[paper: doi, local] [artifact: benchmark] [website]
-
(PLDI 2024)
Concurrent Immediate Reference Counting.
Jaehwang Jung, Jeonghyeon Kim, Matthew J. Parkinson, Jeehoon Kang.
ACM SIGPLAN conference on Programming Languages Design and Implementation.
[paper: doi, local] [artifact: benchmark] [website]
-
(PLDI 2024)
A Proof Recipe for Linearizability in Relaxed Memory Separation Logic.
Sunho Park, Jaewoo Kim, Ike Mulder, Jaehwang Jung, Janggun Lee, Robbert Krebbers, Jeehoon Kang.
ACM SIGPLAN conference on Programming Languages Design and Implementation.
[paper: doi, local] [artifact: Coq proofs]
-
(PLDI 2024)
Modular Hardware Design of Pipelined Circuits with Hazards.
Minseong Jang, Jung In Rhee, Woojin Lee, Shuangshuang Zhao, Jeehoon Kang.
ACM SIGPLAN conference on Programming Languages Design and Implementation.
[paper: doi, local] [website]
-
(OOPSLA 2023)
Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic.
Jaehwang Jung, Janggun Lee, Jaemin Choi, Jaewoo Kim, Sunho Park, Jeehoon Kang.
Object-oriented Programming, Systems, Languages, and Applications.
[paper: doi, local] [artifact: Coq proofs] [website]
-
(SPAA 2023)
Applying Hazard Pointers to More Concurrent Data Structures.
Jaehwang Jung, Janggun Lee, Jeonghyeon Kim, Jeehoon Kang.
ACM Symposium on Parallelism in Algorithms and Architectures.
[paper: doi, local] [artifact: development, benchmark] [website]
-
(PLDI 2023)
Memento: A Framework for Detectable Recoverability in Persistent Memory.
Kyeongmin Cho, Seungmin Jeon, Azalea Raad, Jeehoon Kang.
ACM SIGPLAN conference on Programming Languages Design and Implementation.
[paper: doi, local] [artifact: development] [website]
-
(ASPLOS 2023)
ShakeFlow: Functional Hardware Description with Latency-Insensitive Interface Combinators.
Sungsoo Han†, Minseong Jang†, Jeehoon Kang (†: co-first authors in alphabetical order).
The International Conference on Architectural Support for Programming Languages and Operating Systems.
[paper: doi, local] [artifact: development] [website]
-
(PLDI 2022)
Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic.
Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, Derek Dreyer.
ACM SIGPLAN conference on Programming Languages Design and Implementation.
[paper: doi, local] [website]
-
(2022)
Continuous verification of system of systems with collaborative MAPE-K pattern and probability model slicing.
Jiyoung Song, Jeehoon Kang, Sangwon Hyun, Eunkyoung Jee, Doo-Hwan Bae.
Information and Software Technology.
[paper: doi]
-
(POPL 2022)
Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations.
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer.
ACM SIGPLAN Symposium on Principles of Programming Languages (Distinguished Paper Award).
[paper: doi, local] [website]
-
(PLDI 2021)
Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-x86 and Armv8.
Kyeongmin Cho, Sung-Hwan Lee, Azalea Raad, Jeehoon Kang.
ACM SIGPLAN conference on Programming Languages Design and Implementation.
[paper: doi, local] [artifact: proof, model checker] [website]
-
(PLDI 2020)
A Marriage of Pointer- and Epoch-Based Reclamation.
Jeehoon Kang, Jaehwang Jung.
ACM SIGPLAN conference on Programming Languages Design and Implementation.
[paper: doi, local] [artifact: benchmark] [website]
-
(POPL 2020)
CompCertM: CompCert with Lightweight Modular Verification and Multi-Language Linking.
Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, Chung-Kil Hur.
ACM SIGPLAN Symposium on Principles of Programming Languages.
[paper: doi, local] [website]
-
(POPL 2020)
Stacked Borrows: An Aliasing Model for Rust.
Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer.
ACM SIGPLAN Symposium on Principles of Programming Languages.
[paper: doi, local] [website]
-
(PLOS 2019)
Enveloping Implicit Assumptions of Intrusive Data Structures within Ownership Type System.
Keunhong Lee, Jeehoon Kang, Wonsup Yoon, Joongi Kim, Sue Moon.
Workshop on Programming Languages and Operating Systems.
[paper: doi]
-
(PLDI 2019)
Promising-ARM/RISC-V: a simpler and faster operational concurrency model.
Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, Chung-Kil Hur.
ACM SIGPLAN conference on Programming Languages Design and Implementation.
[paper: doi, local] [website]
-
(Ph.D. Dissertation 2019)
Reconciling low-level features of C with compiler optimizations.
Jeehoon Kang.
Department of Computer Science and Engineering, Seoul National University, Korea.
[paper: handle, local] [website]
-
(PLDI 2018)
Crellvm: Verified Credible Compilation for LLVM.
Jeehoon Kang†, Yoonseung Kim†, Youngju Song†, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur, Kwangkeun Yi (†: co-first authors in alphabetical order).
ACM SIGPLAN conference on Programming Languages Design and Implementation.
[paper: doi, local] [website]
-
(PLDI 2017)
Repairing Sequential Consistency in C/C++11.
Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer.
ACM SIGPLAN conference on Programming Languages Design and Implementation (Distinguished Paper Award).
[paper: doi, local] [website]
-
(POPL 2017)
A Promising Semantics for Relaxed-Memory Concurrency.
Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer.
ACM SIGPLAN Symposium on Principles of Programming Languages.
[paper: doi, local] [website]
-
(POPL 2016)
Lightweight Verification of Separate Compilation.
Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis.
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.
[paper: doi, local] [website]
-
(PLDI 2015)
A Formal C Memory Model Supporting Integer-Pointer Casts.
Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis.
ACM SIGPLAN Conference on Programming Languages Design and Implementation.
[paper: doi, local] [website]
-
(TOPLAS 2014)
Global Sparse Analysis Framework.
Hakjoo Oh, Kihong Heo, Wonchan Lee, Woosuk Lee, Daejun Park, Jeehoon Kang, Kwangkeun Yi.
ACM Transactions on Programming Languages and Systems Volume 36, Issue 3.
[paper: doi] [website]
-
(2012)
A Dice Rolling Game on a Set of Tori.
Jeehoon Kang, Suh-Ryung Kim, Boram Park.
Electrical Journal of Combinatorics Volume 19, Issue 1.
[paper: doi]
People
Alumni
Lectures
- CS220: Programming Principles (2023-2021 Fall)
- CS230: System Programming (2021 Spring)
- CS420: Compiler Design (2023, 2022, 2020 Spring)
- CS431: Concurrent Programming (2023-2019 Fall)
- CS492: Microarchitecture Design (2024 Fall)
- CS500: Design and Analysis of Algorithm (2019 Spring)
Contact
-
Place:
Rm. 4433 (Jeehoon) and Rm. 4441 (students), Bldg. E3-1
School of Computing, KAIST
291 Daehak-ro, Yuseong-gu
Daejeon 34141, Korea -
Phone:
+82-42-350-3578 (Jeehoon)
+82-42-350-7878 (Students) - Comments: