DC Field | Value | Language |
---|---|---|
dc.contributor.advisor | 강지훈 | - |
dc.contributor.author | Lee, Janggun | - |
dc.contributor.author | 이장건 | - |
dc.date.accessioned | 2024-07-30T19:31:46Z | - |
dc.date.available | 2024-07-30T19:31:46Z | - |
dc.date.issued | 2024 | - |
dc.identifier.uri | http://library.kaist.ac.kr/search/detail/view.do?bibCtrlNo=1097264&flag=dissertation | en_US |
dc.identifier.uri | http://hdl.handle.net/10203/321684 | - |
dc.description | 학위논문(석사) - 한국과학기술원 : 전산학부, 2024.2,[iv, 33p :] | - |
dc.description.abstract | Concurrent sets are a fundamental building block of various programs running on multithreaded systems. The most important concurrent set is Harris's list, a lock-free linked list that introduced many key ideas in concurrent set design. Such concurrency allows for highly performant programs, but it also introduces a much higher risk of bugs. Hence, it is important to formally verify the correctness of concurrent sets, in particular of Harris's list. However, there is no work on proving Harris's list that proved a strong specification, is foundational with a minimal trusted computing base, and properly handles memory reclamation at the same time. In this thesis, we present a formal verification of Harris's list in the concurrent separation logic Iris. We prove the linearizability of Harris's list, the de facto correctness criterion for concurrent data structures. All of our work is mechanized in the Coq proof assistant, providing a proof that is done with a minimal trusted computing base. Our implementation handles memory reclamation by utilizing RCU, a safe memory reclamation scheme that is widely used in concurrent data structures. Thus, this thesis presents the first proof of Harris's list that satisfied all of the aforementioned properties. | - |
dc.language | eng | - |
dc.publisher | 한국과학기술원 | - |
dc.subject | 분리 논리 | - |
dc.subject | 자료 구조 | - |
dc.subject | 프로그램 논리 | - |
dc.subject | 엄밀한 검증 | - |
dc.subject | 동시성 | - |
dc.subject | Concurrency▼aFormal verification▼aProgram logic▼aData structures▼aSeparation logic | - |
dc.title | Formal verification of concurrent lists in concurrent separation logic | - |
dc.title.alternative | 동시성 리스트들을 동시성 분리 논리로 엄밀하게 검증하기 | - |
dc.type | Thesis(Master) | - |
dc.identifier.CNRN | 325007 | - |
dc.description.department | 한국과학기술원 :전산학부, | - |
dc.contributor.alternativeauthor | Kang, Jeehoon | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.