논문리뷰: Safety and Liveness of MCS Lock—Layer by Layer

• 정형검증(Formal Verification) : 수학적 증명 기법을 사용하여 시스템의 속성 검증
• 동시성 프로그램 검증 (Verifying Concurrent program)
• by 인증된 동시 추상화 계층(Verifying the MCS Lock Algorithm)

📕 Summary

Problem (summarize)

Verifying concurrent programs poses challenges due to their complexity and potential for non-deterministic behavior.

Solution (This paper's keywork, key insight)

By modularizing the verification process, it becomes easier to reason about different aspects of the program and handle complex operations like thread scheduling and inter-process communication.

• MCS Lock 알고리즘 개발자들은 “인증된 동시 추상화 계층(Verifying the MCS Lock Algorithm)” 이라는 특수 방법을 사용하여 알고리즘이 신뢰할 수 있고 대형 컴퓨터 시스템에서 사용할 수 있는지 확인했습니다. 이 방법을 사용하면 문제를 더 작은 부분으로 나누므로 이해하기 쉽고, 실수가 없는지 확인할 수 있습니다.
• MCS Lock 알고리즘을 CertiKOS 시스템의 다른 부분과 결합하여 훨씬 더 크고 복잡한 컴퓨터 프로그램을 만들 수 있습니다. 컴퓨터가 올바르고 효율적으로 작동하는지 확인하는 데 중요한 도구입니다

알고리즘의 Execution 순서
(b)Free 상태를 CPU 1이 획득하는 것으로 시작
이후 CPU 2(c)와 3(d) 이 잠금을 획득하려고 시도하고 마지막 값이 올바르게 업데이트됩니다.
대기열에 있는 이전 노드의 다음 포인터를 업데이트하는 데 지연이 발생하여 다음 포인터가 설정되지 않을 수 있습니다.
알고리즘은 공정하고 활성 속성(liveness property)을 만족하므로 제한된 시간 내에 mcs 획득 또는 mcs release가 성공할 수 있습니다.

Implementing and Verifying the MCS Lock Algorithm!

Data Structure and the implementation of MCS Lock (in C)

• MCS Lock 알고리즘은 다중 CPU 컴퓨터에 공정하고 확장 가능한 뮤텍스 메커니즘을 제공하는 목록 기반 대기열 잠금입니다.FIFO 순서를 보장하고 CPU가 요청한 순서와 동일한 순서로 잠금을 수신하도록 합니다.
• MCS Lock 알고리즘의 구현은 기계화된 증명을 사용하여 엄격하게 검증되었습니다.이 검증 프로세스는 문제를 모듈화하고 분리할 수 있는 인증된 동시 추상화 계층의 방법론을 따릅니다.
• 검증 프로세스: 저수준 기계 모델, 데이터 추상화, 동시 인터리빙에 대한 추론 등 여러 계층으로 증명을 분할하는 작업이 포함됩니다. (이러한 분리 덕분에 계층화된 방법론은 CertiKOS 커널과 같은 대규모 시스템의 검증된 프로그래밍에 적합합니다.)

Contribution