cp.kaist.ac.kr Open in urlscan Pro
143.248.135.193  Public Scan

Form analysis
0 forms found in the DOM

Text Content

KAIST CP Menu
 * Home
 * Join
 * Projects
 * Publications
 * People
 * Lectures
 * Contact


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, Changu Kang, Janggun Lee, Hakjoo Oh, Jeehoon
   Kang.
   Object-oriented Programming, Systems, Languages, and Applications. (to
   appear).
   
   

 * (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


Jeehoon Kang
Principal Investigator
 * 
 * 
 * 
 * 
 * 
 * 
 * 


Jaehwang Jung
Ph.D. Student
 * 
 * 
 * 
 * 


Shuangshuang Zhao
Ph.D. Student
 * 
 * 
 * 
 * 


Seungmin Jeon
Ph.D. Student
 * 
 * 
 * 
 * 
 * 


Janggun Lee
Ph.D. Student
 * 
 * 
 * 
 * 


Minseong Jang
Ph.D. Student
 * 
 * 
 * 
 * 


Jung In Rhee
M.S. Student
 * 
 * 
 * 
 * 


Haechan An
M.S. Student
 * 
 * 
 * 
 * 


Woojin Lee
M.S. Student
 * 
 * 
 * 
 * 


Taewoo Kim
M.S. Student
 * 
 * 
 * 
 * 


Sunho Park
M.S. Student
 * 
 * 
 * 
 * 


Jaewoo Kim
M.S. Student
 * 
 * 
 * 
 * 


Jeonghyeon Kim
M.S. Student
 * 
 * 
 * 
 * 


Gieun Jeong
M.S. Student
 * 
 * 
 * 
 * 


Jonguk Jeon
B.S. Student
 * 
 * 
 * 


Sungjae Im
B.S. Student
 * 
 * 
 * 


Subeen Park
B.S. Student
 * 
 * 
 * 


Pablo Robin Guerrero
B.S. Student
 * 
 * 
 * 
 * 


Taeyun Kim
B.S Student
 * 
 * 
 * 
 * 


Wonhyeok Ko
B.S Student
 * 
 * 
 * 
 * 


Jeho Yeon
B.S. Student
 * 
 * 
 * 





ALUMNI

Kyeongmin Cho, Ph.D.
(first occupation: Rebellions)
 * 
 * 
 * 
 * 
 * 

Jaemin Choi, M.S.
(first occupation: FuriosaAI)
 * 
 * 
 * 
 * 

Chunmyong Park, M.S.
(first occupation: Supertone)
 * 
 * 
 * 
 * 

Sungsoo Han, M.S.
(first occupation: FuriosaAI)
 * 
 * 
 * 

Sunghwan Shim, M.S.
(first occupation: FuriosaAI)
 * 
 * 
 * 

Sunghyuk Kay, M.S.
(first occupation: LG Electronics)
 * 
 * 
 * 
 * 

Yeji Han, B.S.
(first occupation: Software Foundations Laboratory, SNU)
 * 
 * 
 * 

Doehyun Baek, B.S.
(first occupation: Programming Language Research Group, KAIST)
 * 
 * 
 * 

Jungwoo Kim, B.S.
(first occupation: Computer Architecture and Systems Laboratory, KAIST)
 * 
 * 
 * 





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)
 * Comments:
   


 * KAIST
 * KAIST School of Computing

Content on this site is licensed under a CC BY 4.0 License. | Theme: Petridish