3 papers
cs.PL2026
High-Level Synthesis of Efficient Pipelines with Visibility Control
Jungin Rhee, Minseong Jang, Jaewoo Kim +1
High-level synthesis (HLS) raises the abstraction of hardware design from concurrent register-transfer level (RTL) programs to sequential programs. Among the forms of parallelism H…
cs.PL2026
Formal Verification of an Out-of-Order Multiprocessor against an In-Order Weak-Memory ISA
Janggun Lee, Jeehoon Kang
Out-of-order multiprocessor is a critical piece of modern hardware, and their verification must solve the following challenges. First, inter-core interleaving, in which the order t…
cs.PL2022
Practical Detectability for Persistent Lock-Free Data Structures
Kyeongmin Cho, Seungmin Jeon, Jeehoon Kang
Persistent memory (PM) is an emerging class of storage technology that combines the benefits of DRAM and SSD. This characteristic inspires research on persistent objects in PM with…