Concurrency and Parallelism

We design and verify innovative concurrent and parallel systems.

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:

  • 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

  • (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] ​ ​
  • (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
  • :house:
  • :love_letter:
  • :octocat:
Kyeongmin Cho
Ph.D. Student
  • :house:
  • :love_letter:
  • :octocat:
Jaehwang Jung
Ph.D. Student
  • :house:
  • :love_letter:
  • :octocat:
Shuangshuang Zhao
Ph.D. Student
  • :house:
  • :love_letter:
  • :octocat:
Seungmin Jeon
M.S. Student
  • :house:
  • :love_letter:
  • :octocat:
Janggun Lee
M.S. Student
  • :house:
  • :love_letter:
  • :octocat:
Minseong Jang
M.S. Student
  • :house:
  • :love_letter:
  • :octocat:
Jung In Rhee
M.S. Student
  • :house:
  • :love_letter:
  • :octocat:
Haechan An
M.S. Student
  • :house:
  • :love_letter:
  • :octocat:
Woojin Lee
M.S. Student
  • :house:
  • :love_letter:
  • :octocat:
Taewoo Kim
B.S. Student
  • :house:
  • :love_letter:
  • :octocat:
Sunho Park
B.S. Student
  • :house:
  • :love_letter:
  • :octocat:
Jaewoo Kim
B.S. Student
  • :house:
  • :love_letter:
  • :octocat:
Jeonghyeon Kim
B.S. Student
  • :house:
  • :love_letter:
  • :octocat:
Gieun Jeong
B.S. Student
  • :house:
  • :love_letter:
  • :octocat:
Kisoo Kim
B.S. Student
  • :house:
  • :love_letter:
  • :octocat:


Alumni

Jaemin Choi, M.S.
(first occupation: FuriosaAI)
  • :house:
  • :love_letter:
  • :octocat:
Chunmyong Park, M.S.
(first occupation: Supertone)
  • :house:
  • :love_letter:
  • :octocat:
Sungsoo Han, M.S.
(first occupation: FuriosaAI)
  • :house:
  • :love_letter:
  • :octocat:
Sunghwan Shim, M.S.
(first occupation: FuriosaAI)
  • :house:
  • :love_letter:
  • :octocat:
Sunghyuk Kay, M.S.
(first occupation: LG Electronics)
  • :house:
  • :love_letter:
  • :octocat:
Yeji Han, B.S.
  • :house:
  • :love_letter:
  • :octocat:
Doehyun Baek, B.S.
(first occupation: Programming Language Research Group, KAIST)
  • :house:
  • :love_letter:
  • :octocat:
Jungwoo Kim, B.S.
(first occupation: Computer Architecture and Systems Lab, KAIST)
  • :house:
  • :love_letter:
  • :octocat:


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: