Concurrency and Parallelism

We’re actively recruiting motivated students of all levels interested in designing and verifying concurrent and parallel systems. If you’re interested, please read this instruction and contact Jeehoon ASAP.

Projects

In the era of big data, artificial intelligence, and internet of things, humankind requires more and more computing resources, but they are becoming more and more scarce due to the slowing of Dennard scaling and Moore’s law. The only way to meet the demand is to massively parallelize computing resources to mitigate the damages of the slowing.

So we aim to design, implement, and verify such massively parallel systems, from microarchitectures to programming languages to algorithms, that greatly improves the performance and significantly reduces power consumption over conventional systems.

Our general strategy in attacking this goal is (1) to holistically understand the entire computer systems; (2) to design abstraction layers that realize the intrinsic parallelism of the workloads while providing easy programming environment at the same time; and (3) to formally verify such abstraction layers so that the users can use the them safely and fearlessly.

Specifically, we are working on design and verification of concurrent and parallel systems:

• Designing concurrent and parallel systems: It is difficult to develop efficient and yet safe concurrent software and hardware, because efficient systems should allow concurrent accesses from multiple threads or components that complicate the reasoning of safety.

  So we are developing design principles for coordinating concurrent accesses, and based on the design principles, building practical concurrent systems. Specifically, we are building:

  • AI serving systems, optimized for NPUs (with FuriosaAI)
  • Operating systems in Rust, safe by construction (with Google)
  • Persistent memory library, with solid design principles (with ETRI)
  • Concurrent garbage collector, with high throughput and low latency

  • FPGA high-performance networking systems, easily programmable

• Verifying concurrent and parallel systems: It is difficult to ensure the safety of concurrent software and hardware by testing because they exhibit so many behaviors due to inherent nondeterminism arising from scheduling, optimization, or other factors.

  So we are designing verification techniques for proving the correctness of concurrent systems and verify real-world systems—such as operating systems, database systems, or cache coherence protocols, thereby answering the following research question: is verification more cost-effective than testing for concurrent systems? Specifically, we are verifying:

  • Persistent memory library (with ETRI)
  • Strong specification of concurrent data structures (with MPI-SWS)
  • Strong specification of concurrent garbage collectors
  • Compilers for concurrent programs

Publications

• (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] ​ ​
  

• (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] ​
  

• (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)
• 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)
• Helpdesk
• Comments: Do you want to talk to us here? Feel free to leave a comment!