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
PhD Student
  • :house:
  • :love_letter:
  • :octocat:
Jaehwang Jung
PhD Student
  • :house:
  • :love_letter:
  • :octocat:
Shuangshuang Zhao
PhD Student
  • :house:
  • :love_letter:
  • :octocat:
Seungmin Jeon
Master Student
  • :house:
  • :love_letter:
  • :octocat:
Janggun Lee
Master Student
  • :house:
  • :love_letter:
  • :octocat:
Minseong Jang
Master Student
  • :house:
  • :love_letter:
  • :octocat:
Jung In Rhee
Master Student
  • :house:
  • :love_letter:
  • :octocat:
Haechan An
Master Student
  • :house:
  • :love_letter:
  • :octocat:
Taewoo Kim
Undergraduate Student
  • :house:
  • :love_letter:
  • :octocat:
Woojin Lee
Master Student
  • :house:
  • :love_letter:
  • :octocat:
Sunho Park
Undergraduate Student
  • :house:
  • :love_letter:
  • :octocat:
Jaeyong Sung
Undergraduate Student
  • :house:
  • :love_letter:
  • :octocat:
Jaewoo Kim
Undergraduate Student
  • :house:
  • :love_letter:
  • :octocat:
Jeonghyeon Kim
Undergraduate Student
  • :house:
  • :love_letter:
  • :octocat:
Kisoo Kim
Undergraduate Student
  • :house:
  • :love_letter:
  • :octocat:


Alumni

Jaemin Choi
Master Student (first occupation: FuriosaAI)
  • :house:
  • :love_letter:
  • :octocat:
Chunmyong Park
Master Student (first occupation: Supertone)
  • :house:
  • :love_letter:
  • :octocat:
Sungsoo Han
Master Student (first occupation: FuriosaAI)
  • :house:
  • :love_letter:
  • :octocat:
Sunghwan Shim
Master Student (first occupation: FuriosaAI)
  • :house:
  • :love_letter:
  • :octocat:
Yeji Han
Undergraduate Student
  • :house:
  • :love_letter:
  • :octocat:
Doehyun Baek
Undergraduate Student (first occupation: Programming Language Research Group, KAIST)
  • :house:
  • :love_letter:
  • :octocat:
Sunghyuk Kay
Master Student (first occupation: LG Electronics)
  • :house:
  • :love_letter:
  • :octocat:
Jungwoo Kim
Undergraduate Student (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)
  • :scream: Helpdesk
  • :speaking_head: Comments: Do you want to talk to us here? Feel free to leave a comment!