Research
My mission as a computer scientist is to
formally understand the underlying
principles of real-world computer systems, thereby
helping programmers to
write and reason about those systems. For my Ph.D., I have primarily focused on formally
understanding non-blocking
concurrent programming, which is an essential
ingredient for exploiting
parallelism and is becoming more and more important
since the slowdown of Moore's law. In the future, as an independent researcher, I would like
to apply the understanding of concurrency to building practical verification/analysis tools
for concurrent programs. I believe my research will have far-reaching impact on the way the
IT industry develops system software.
I am maintaining
the Crossbeam
project, which serves as the
de facto standard concurrency library
for
the Rust programming language. I am also writing a
compiler for
Furiosa AI's MadRun deep learning accelerator.
Publications
-
Promising-ARM/RISC-V: a simpler and faster operational concurrency model.
Christopher Pulte,
Jean Pichon-Pharabod,
Jeehoon Kang,
Sung-Hwan Lee,
Chung-Kil Hur.
To appear in Proceedings of the 40th annual ACM SIGPLAN conference on Programming Languages Design and Implementation (PLDI 2019). (conditionally accepted)
[project page]
-
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.
* The first three authors contributed equally and are listed alphabetically.
In Proceedings of the 39th annual ACM SIGPLAN conference on Programming Languages Design and Implementation (PLDI 2018).
[paper] [project page]
-
Repairing Sequential Consistency in C/C++11.
Ori Lahav,
Viktor Vafeiadis,
Jeehoon Kang,
Chung-Kil Hur,
Derek Dreyer.
In Proceedings of the 38th annual ACM SIGPLAN conference on Programming Languages Design and Implementation (PLDI 2017).
ACM SIGPLAN PLDI Distinguished Paper Award.
[paper] [project page]
-
A Promising Semantics for Relaxed-Memory Concurrency.
Jeehoon Kang,
Chung-Kil Hur,
Ori Lahav,
Viktor Vafeiadis,
Derek Dreyer.
In Proceedings of the 44th annual ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017).
[paper] [project page]
-
Lightweight Verification of Separate Compilation.
Jeehoon Kang,
Yoonseung Kim,
Chung-Kil Hur,
Derek Dreyer,
Viktor Vafeiadis.
In Proceedings of the 43rd annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016).
[paper] [project page]
-
A Formal C Memory Model Supporting Integer-Pointer Casts.
Jeehoon Kang,
Chung-Kil Hur,
William Mansky,
Dmitri Garbuzov,
Steve Zdancewic,
Viktor Vafeiadis.
In Proceedings of the 36th annual ACM SIGPLAN conference on Programming Languages Design and Implementation (PLDI 2015)..
[paper] [project page]
-
Global Sparse Analysis Framework.
Hakjoo Oh,
Kihong Heo,
Wonchan Lee,
Woosuk Lee,
Daejun Park,
Jeehoon Kang,
Kwangkeun Yi.
In ACM Transactions on Programming Languages and Systems vol. 36, Issue 3, 2014 (TOPLAS), September 2014.
[paper]
-
A Dice Rolling Game on a Set of Tori.
Jeehoon Kang,
Suh-Ryung Kim,
Boram Park.
In Electrical Journal of Combinatorics Volume 19, Issue 1, 2012.
[paper]
Invited Talks
-
iRRAM-Coq: Fearless Verification of Exact Real Arithmetic Programs.
In the 1st Workshop on Real Verification (RV 2017).
[development]