충돌 없는 복제 데이터 타입 (CRDT)을 위한 Datalog 프레임워크

분산 애플리케이션 (Distributed applications)은 공유 데이터에 대해 로컬 우선 협업 (local-first collaboration)을 점점 더 많이 지원하고 있으며, 이를 통해 여러 사용자가 전역적인 조정 (global coordination) 없이 동시에 업데이트를 수행할 수 있습니다. 이러한 협업은 동시적 상호작용 (concurrent interactions)의 의도된 의미론 (semantics)을 포착하기 위해 세심한 설계가 필요합니다. 본 논문에서는 충돌 없는 복제 데이터 타입 (Conflict-Free Replicated Data Types, CRDTs) 및 CRDT 기반 애플리케이션의 의미론을 명시하고 추론하기 위한 선언적 프레임워크 (declarative framework)를 Datalog에서 소개합니다. 이 프레임워크는 CRDT의 의미론을 작업 컨텍스트 (operation contexts)에 대한 실행 가능한 논리 프로그램 (executable logic programs)으로 모델링하여, 동시성을 명시적이고 구성 가능하게 (compositional) 만들며, 따라서 자동화된 분석 (automated analysis)이 가능하도록 합니다. 하나의 응용 사례로서, 우리는 속성 기반 테스트 (property-based testing)를 사용하여 구현체들을 비교합니다. 우리가 아는 바로는, 이는 복잡한 CRDT 및 그 구성 (compositions)을 프로토타이핑하고 분석하기 위한 기반으로 Datalog를 체계적으로 사용한 첫 번째 연구입니다. 우리는 협업 그래프 데이터 편집 (collaborative graph data editing) 사례 연구를 사용하여 우리의 방법론을 평가하며, 작업 및 복제본 (replicas)의 수가 증가함에 따른 정확성 검증 (correctness validation) 및 확장성 (scalability)을 평가한 실험 결과를 보고합니다.