선형 가시성(Linearizability)은 동시 데이터 구조에 대한 표준적인 정확성 조건입니다. 이는 연산이 호출되고 반환되는 지점 사이의 어떤 원자적 순간에 효과가 발생한 것처럼 동작함을 보장합니다. 선형 가시성이 핵심적인 역할을 함에도 불구하고, 이전 연구에서는 대신 논리의 추론 규칙 측면에서 연산의 원자성을 내재화하는 사양 스타일인 '논리적 원자성(logical atomicity)'을 사용하는 것이 좋다고 주장해 왔습니다. 이러한 논리적으로 원자적인 사양은 선형 가시성보다 논리 내부에서 구성하기가 더 쉬하도록 의도되었습니다. 이전 연구에서는 Iris 분리 논리(separation logic) 프레임워크 내에서 특정 형태의 논리적 원자적 사양이 데이터 구조가 선형화 가능함(linearizable)을 함의한다는 것을 보여주었습니다. 하지만 그 역은 미해결 문제로 남아 있었습니다: 모든 선형화 가능한 데이터 구조에 대해, 대응하는 논리적 원자적 사양을 항상 도출할 수 있는가? 본 논문은 이 질문을 긍정적으로 해결합니다. 우리는 임의의 선형화 가능한 데이터 구조에 대해 논리적 원자적 사양을 도출하는 Iris를 위한 완전성 정리(completeness theorem)를 증명합니다. 그 결과, 다양한 선형 가시성 증명 기법들을 Iris에 임베딩하고 이를 사용하여 논리적 원자적 사양을 도출할 수 있게 됩니다. 우리는 이 방법을 세 가지 선형화성 증명 방법—측면 지향(aspect-oriented) 선형화성 증명, 커밋 포인트가 있는 순방향 시뮬레이션(forward simulations with commit points), 그리고 메타 구성 추적(meta-configuration tracking)—에 적용합니다. 이러한 임베딩을 사용하여 Herlihy-Wing 큐와 Baskets Queue에 대한 논리적 원자적 사양을 도출합니다. 나아가, 우리는 논리적 원자성과 Iris에서 사용되어 온 이전의 논리 관계 모델에서의 리파인먼트(refinement) 인코딩 간의 연결 고리를 확립합니다. 이 결과는 우리가 논리적 원자적 사양을 리파인먼트 전반에 걸쳐 전달할 수 있게 해주며, 이를 Folly MPMC 큐 구현에 적용합니다. 본 논문의 모든 결과는 Rocq Prover에서 기계화되었습니다.