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:

  • 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:

Publications

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

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
Subeen Park
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

Contact

  • :office: Place:
         Rm. 4433 (Jeehoon) and Rm. 4441 (students), Bldg. E3-1
         School of Computing, KAIST
         291 Daehak-ro, Yuseong-gu
         Daejeon 34141, Korea
  • :phone: Phone:
         +82-42-350-3578 (Jeehoon)
         +82-42-350-7878 (Students)
  • :speaking_head: Comments: