선형성

이 문서에는 일반적인 참조 목록이 포함되어 있지만 대응하는 충분한 인라인 인용이 없습니다. 좀 더 정밀한 인용문을 도입하여 이 기사의 개선에 협조해 주십시오.(2010년 12월) (이 템플릿메시지의 삭제 방법과 삭제 타이밍에 대해 알아보기)

이 문서에서는 다른 문서의 범위, 특히 serializability와 atomicity(데이터베이스 시스템)를 복제합니다. 토크 페이지에서 논의 후 Wikipedia의 스타일 매뉴얼(2018년 11월)에 맞게 편집 부탁드립니다.

동시 프로그래밍에서 연산(또는 연산 세트)은 다음과 같은 응답 이벤트를 추가하여 확장할 수 있는 호출 및 응답 이벤트(이벤트)의 순서 목록으로 구성될 경우 선형화할 수 있습니다.

1. 확장 리스트는, 시퀀셜 이력으로서 재표현할 수 있습니다(시리얼화 가능).
2. 이 순차 이력은 원래 확장되지 않은 목록의 하위 집합입니다.

비공식적으로 이는 수정되지 않은 이벤트 목록은 호출이 직렬화 가능한 경우에만 선형화가 가능하지만 직렬 일정의 응답 중 일부가 아직 ^[1]반환되지 않은 경우에만 선형화가 가능하다는 것을 의미합니다.

동시 시스템에서 프로세스는 공유 객체에 동시에 액세스할 수 있습니다.여러 프로세스가 단일 개체에 액세스하기 때문에 한 프로세스가 개체에 액세스하는 동안 다른 프로세스가 개체의 내용을 변경하는 상황이 발생할 수 있습니다.시스템을 선형화할 수 있도록 하는 것이 이 문제의 해결책 중 하나입니다.선형화 가능한 시스템에서는 공유 객체에서 작업이 겹치더라도 각 작업은 즉시 수행되는 것으로 보입니다.선형화 가능성은 강력한 정확성 조건이며, 여러 프로세스에서 동시에 개체에 액세스할 때 가능한 출력을 제한합니다.이것은 작업이 예기치 않게 또는 예측할 수 없는 방식으로 완료되지 않도록 하는 안전 속성입니다.시스템이 선형화할 수 있는 경우 프로그래머가 시스템에 ^[2]대해 추론할 수 있습니다.

선형화의 역사

선형성은 1987년 Herlihy와 Wing에 의해 일관성 모델로 처음 도입되었습니다.그것은 "원자 연산은 동시 연산에 의해 중단될 수 없는 것(또는 중단되지 않는 것)"과 같은 원자 연산의 보다 제한적인 정의를 포함하며, 이것은 일반적으로 언제 연산이 시작되고 끝나는 것으로 간주되는지에 대해 모호하다.

원자 객체는 순차적 정의에서 항상 연속적으로 발생하는 일련의 연산이 병렬로 실행되므로 즉시 완전히 이해할 수 있습니다. 불일치는 발생하지 않습니다.특히 선형성은 시스템의 불변성이 모든 운영에서 관찰되고 유지되도록 보장합니다. 모든 운영이 개별적으로 불변성을 보존하면 시스템 전체가 보존됩니다.

선형화의 정의

동시 시스템은 공유 데이터 구조 또는 객체를 통해 통신하는 프로세스의 집합으로 구성됩니다.동시에 여러 프로세스에 의해 객체에 액세스할 수 있는 이러한 동시 시스템에서는 선형성이 중요하며 프로그래머는 예상되는 결과에 대해 추론할 수 있어야 합니다.동시 시스템의 실행은 완료된 동작의 순서 순서인 이력(history)을 낳는다.

기록은 스레드 또는 프로세스 집합에 의해 객체로 만들어진 호출 및 응답의 시퀀스입니다.호출은 조작의 개시라고 생각할 수 있으며, 응답은 그 조작의 시그널링 종료라고 할 수 있습니다.함수의 각 호출에는 후속 응답이 있습니다.이것은 오브젝트의 사용을 모델링하는 데 사용할 수 있습니다.예를 들어, A와 B라는 두 개의 스레드가 모두 잠금을 잡으려고 시도하고 이미 잠긴 경우 이를 취소한다고 가정합니다.이는 두 스레드 모두 잠금 작업을 호출하고 두 스레드 모두 응답을 수신하는 것으로 모델링됩니다(한 개는 성공, 한 개는 실패).

A가 잠금을 호출하다

B가 잠금을 호출합니다.

A가 "실패" 응답을 수신하다

B가 "성공적" 응답을 얻다

순차 이력은 모든 호출에 즉각적인 응답이 있는 기록입니다. 즉, 호출과 응답이 즉시 발생하는 것으로 간주됩니다.순차적 이력은 실제 동시성이 없기 때문에 추론하기에는 사소한 것이어야 합니다. 앞의 예는 순차적이지 않기 때문에 추론하기 어렵습니다.여기서 선형성이 요구됩니다.

다음과 같이 완료된 연산의 선형 순서$$order(\$displaystyle \sigma)$가 있는 경우 이력을 선형화할 수 있습니다.

1. For every completed operation in ${\displaystyle \sigma }$, the operation returns the same result in the execution as the operation would return if every operation was completed one by one in order ${\displaystyle \sigma }$.
2. op이 개시(호출₁)되기 전에₂ op이 완료(응답 취득)된 경우₁$op$은 op보다₂ 우선합니다(\$displaystyle \sigma$^[1] 。

즉, 다음과 같습니다.

• 호출 및 응답 순서를 변경하여 순차 이력을 생성할 수 있습니다.
• 객체의 순차적 정의에 따라 순차적 이력이 올바른지 여부
• 원래 이력에서 호출 전에 응답이 있었을 경우, 순차적인 순서 변경에서 응답이 호출 전에 응답해야 합니다.

(여기서 처음 2개의 항목은 시리얼라이저빌리티와 일치합니다.작업은 어떤 순서로 이루어지는 것 같습니다.이는 선형성 특유의 마지막 점이며, 따라서 Herlihy와 Wing의 주요 공헌이다.)^[1]

위의 잠금 예제를 다시 정렬하는 두 가지 방법을 살펴보겠습니다.

A가 잠금을 호출하다

A가 "실패" 응답을 수신하다

B가 잠금을 호출합니다.

B가 "성공적" 응답을 얻다

A의 응답보다 낮은 B의 호출 순서를 지정하면 순차 이력이 생성됩니다.모든 작업이 명확한 순서로 이루어지기 때문에 이는 쉽게 이해할 수 있습니다.유감스럽게도 오브젝트의 순차적 정의와 일치하지 않습니다(프로그램의 의미와 일치하지 않습니다.A는 잠금을 정상적으로 취득하고 B는 그 후에 중단해야 합니다.

B가 잠금을 호출합니다.

B가 "성공적" 응답을 얻다

A가 잠금을 호출하다

A가 "실패" 응답을 수신하다

이것은 또 하나의 올바른 순차 이력입니다.선형화이기도 합니다!리니어 사이저빌리티의 정의에서는 호출 전에 응답이 없었기 때문에 호출 전에 응답이 없었기 때문에 원하는 대로 순서를 변경할 수 있습니다.그러므로 원래의 역사는 실로 선형화할 수 있다.

오브젝트(이력과는 반대)는 사용의 모든 유효한 이력을 선형화할 수 있는 경우 선형화할 수 있습니다.이것은 증명하기 훨씬 어려운 주장이라는 점에 유의하십시오.

리니어라이저빌리티와 비교

잠금과 상호 작용하는 두 개체의 이력을 다시 살펴보겠습니다.

A가 잠금을 호출하다

A이(가) 정상적으로 잠김

B가 잠금 해제를 호출하다

B가 정상적으로 잠금 해제되었습니다.

A가 잠금을 해제하다

A가 정상적으로 잠금 해제되었습니다.

이 이력은 A와 B가 모두 잠금을 유지하는 지점이 있기 때문에 유효하지 않습니다.또한 순서 규칙을 위반하지 않고 유효한 순서 이력으로 순서를 변경할 수 없습니다.따라서 선형화할 수 없습니다.그러나 시리얼라이제빌리티에서는 B의 잠금 해제 조작을 A의 원래 잠금 이전으로 이동할 수 있습니다(개체가 잠금 상태에서 기록을 시작한다고 가정).

B가 잠금 해제를 호출하다

B가 정상적으로 잠금 해제되었습니다.

A가 잠금을 호출하다

A이(가) 정상적으로 잠김

A가 잠금을 해제하다

A가 정상적으로 잠금 해제되었습니다.

A와 B 사이에 대체적인 통신 수단이 없는 한, 이 순서 변경은 타당합니다.정렬 제한으로 인해 여러 개의 선형 가능한 개체가 전체적으로 선형 가능한 상태로 유지되므로 개별 개체를 별도로 고려할 때 선형화 가능성이 더 우수합니다.

선형화 점

선형화의 정의는 다음과 같습니다.

• 모든 함수 호출에는 호출과 응답 사이에 선형화 포인트가 있습니다.
• 모든 함수는 선형화 지점에서 즉시 발생하며 순차 정의에 지정된 대로 작동합니다.

이 대안은 보통 증명하기가 훨씬 쉽습니다.사용자로서 추론하기도 훨씬 쉬운데, 그 주된 이유는 직감 때문이다.순간적으로 또는 불가분하게 발생하는 이러한 특성은 더 긴 "선형화 가능"^[1]의 대안으로 원자라는 용어를 사용하게 한다.

다음 예에서는 비교 및 스왑을 기반으로 구축된 카운터의 선형화 지점이 첫 번째 성공적인 비교 및 스왑 업데이트의 선형화 지점입니다.잠재적으로 충돌할 수 있는 모든 작업은 해당 기간 동안 실행에서 제외되므로 잠금을 사용하여 구축된 카운터는 잠금이 유지되는 동안 언제든지 선형화하는 것으로 간주할 수 있습니다.

원시 원자 명령

^{[어디까지?]}

프로세서에는 잠금 및 잠금 프리 및 대기 프리 알고리즘을 구현하는 데 사용할 수 있는 명령이 있습니다.인터럽트를 일시적으로 금지하고 현재 실행 중인 프로세스를 컨텍스트스위칭할 수 없도록 하는 기능도 유니프로세서로 충분합니다.이러한 명령어는 컴파일러 및 운영체제 라이터에 의해 직접 사용되지만 고급 언어에서는 바이트 코드 및 라이브러리 함수로 추상화 및 공개됩니다.

• 아토믹 읽기/쓰기
• 원자 교환(일부 Burroughs 메인프레임의 RDLK 명령 및 XCHG x86 명령)
• 테스트 및 세트
• 가져오기 및 추가
• 비교 및 비교
• load-link/store-conditional.

대부분의^{[citation needed]} 프로세서에는 메모리에 대해 원자적이지 않은 저장소 작업이 포함되어 있습니다.여기에는 여러 단어 저장소 및 문자열 작업이 포함됩니다.저장소의 일부가 완료되었을 때 우선순위가 높은 인터럽트가 발생하면 인터럽트 레벨이 반환되었을 때 작업을 완료해야 합니다.인터럽트를 처리하는 루틴은 변경되는 메모리를 변경하지 않아야 합니다.인터럽트 루틴을 작성할 때는 이 점을 고려하는 것이 중요합니다.

중단 없이 완료해야 하는 명령이 여러 개 있는 경우 인터럽트를 일시적으로 비활성화하는 CPU 명령이 사용됩니다.인터럽트에 대한 허용 불가능한 응답 시간 또는 인터럽트 손실을 방지하기 위해 이 명령어는 몇 가지 명령으로만 유지되어야 하며 인터럽트를 다시 활성화해야 합니다.멀티프로세서 환경에서는 인터럽트 발생 여부에 관계없이 각 CPU가 프로세스를 방해할 수 있기 때문에 이 메커니즘은 충분하지 않습니다.또한 명령 파이프라인이 있는 경우, Cyrix 혼수 버그와 같이 무한 루프에 연쇄되어 서비스 거부 공격을 일으킬 수 있기 때문에 무정전 동작은 보안 위험을 수반합니다.

C 표준 및 SUSv3는 다음을 제공합니다.sig_atomic_t단순한 아토믹 읽기 및 쓰기의 경우 증가 또는 감소는 ^[3]아토믹하지 않습니다.C11에서는 보다 복잡한 원자 연산을 이용할 수 있으며, 이는stdatomic.h컴파일러는 하드웨어 기능이나 복잡한 방법을 사용하여 작업을 구현합니다.예를 들어 GCC의 libatomic이 있습니다.

ARM 명령 집합은 다음을 제공합니다.LDREX그리고.STREX특정 주소에 ^[4]대한 메모리 액세스를 추적하기 위해 프로세서에 구현된 전용 모니터를 사용하여 원자 메모리 액세스를 구현하기 위해 사용할 수 있는 명령입니다.단, 콜 사이에 콘텍스트스위치가 발생한 경우LDREX그리고.STREX매뉴얼에 기재되어 있는 것은 다음과 같습니다.STREX에러가 발생해, 조작을 재시도 할 필요가 있습니다.

고도의 원자력 운용

선형성을 달성하는 가장 쉬운 방법은 중요한 섹션에서 원시 작업 그룹을 실행하는 것입니다.선형성을 위반하지 않는 한 독립적 운영은 신중하게 중요 섹션과 겹치는 것을 허용할 수 있다.이러한 접근방식은 다수의 잠금장치 비용과 병렬화 증가의 이점을 균형 있게 유지해야 한다.

연구자들이 선호하는 또 다른 접근법은 하드웨어가 제공하는 원자를 사용하여 선형화 가능한 객체를 설계하는 것입니다.이는 사용 가능한 병렬성을 극대화하고 동기화 비용을 최소화할 수 있는 잠재력을 가지고 있지만, 물체가 올바르게 동작한다는 것을 보여주는 수학적 증거가 필요합니다.

이 두 가지 중 유망한 하이브리드는 트랜잭션 메모리 추상화를 제공하는 것입니다.중요한 섹션과 마찬가지로 사용자는 다른 스레드와 분리하여 실행해야 하는 순차 코드를 표시합니다.그 후, 실장은 코드가 원자적으로 실행되도록 합니다.이 추상화 스타일은 데이터베이스와 상호작용할 때 흔히 볼 수 있습니다.예를 들어 Spring Framework를 사용할 때 @Transactional을 사용하여 메서드에 주석을 붙이면 폐쇄된 모든 데이터베이스 상호작용이 단일 데이터베이스 트랜잭션에서 수행됩니다.트랜잭션 메모리는 한 걸음 더 나아가 모든 메모리 상호작용이 원자적으로 이루어지도록 보장합니다.데이터베이스 트랜잭션과 마찬가지로 트랜잭션 구성, 특히 데이터베이스 및 메모리 내 트랜잭션과 관련된 문제가 발생합니다.

선형화 가능한 오브젝트를 설계할 때 공통의 주제는 all-or-nothing 인터페이스를 제공하는 것입니다.작업은 완전히 성공하거나 실패하여 아무것도 하지 않습니다.(ACID 데이터베이스는 이 원리를 원자성이라고 부릅니다.)조작이 실패했을 경우(통상은 동시 조작에 의해), 유저는 재시도 할 필요가 있습니다.보통은 다른 조작을 실행합니다.예를 들어 다음과 같습니다.

• Compare-and-Swap은 새 값이 지정된 이전 값과 일치하는 경우에만 해당 위치에 새 값을 씁니다.이것은 일반적으로 읽기 수정 CAS 시퀀스에서 사용됩니다.사용자는 위치를 읽고 새로운 값을 계산하여 CAS(compare-and-swap)에 씁니다.값이 동시에 변경되면 CAS는 실패하고 사용자는 다시 시도합니다.
• load-link/store-conditional은 이 패턴을 보다 직접적으로 부호화합니다.사용자는 load-link를 사용하여 위치를 읽고 새로운 값을 계산하여 store-conditional을 사용하여 씁니다.값이 동시에 변경된 경우 SC(store-conditional)는 실패하고 사용자는 다시 시도합니다.
• 데이터베이스 트랜잭션에서 동시 작업(예를 들어 교착 상태)으로 인해 트랜잭션을 완료할 수 없는 경우 트랜잭션은 중단되고 사용자는 다시 시도해야 합니다.

선형화의 예

카운터

선형화의 힘과 필요성을 입증하기 위해 서로 다른 프로세스가 증가할 수 있는 단순한 카운터를 고려합니다.

여러 프로세스에서 접근할 수 있는 카운터 오브젝트를 구현하고 싶습니다.많은 일반적인 시스템에서는 카운터를 사용하여 이벤트가 발생한 횟수를 추적합니다.

카운터 개체는 여러 프로세스에서 액세스할 수 있으며 두 가지 작업을 사용할 수 있습니다.

1. Increment - 카운터에 저장된 값에 1을 더하고 확인 응답을 반환합니다.
2. 읽기 - 카운터에 저장된 현재 값을 변경하지 않고 반환합니다.

공유 레지스터를 사용하여 이 카운터 개체를 구현하려고 합니다.

우리가 보게 될 첫 번째 시도는 비선형화입니다.프로세스 중 하나의 공유 레지스터를 사용하여 다음과 같이 구현합니다.

비원자

순진한 비원자 구현:

증가:

1. 레지스터 R의 값을 읽습니다.
2. 값에 1을 추가합니다.
3. 새 값을 레지스터 R에 다시 씁니다.

읽기:

레지스터 R 읽기

이 간단한 실장은 다음 예에서 알 수 있듯이 선형화할 수 없습니다.

값 0으로 초기화되어 있는 단일 카운터 오브젝트에 액세스하기 위해 2개의 프로세스가 실행되고 있다고 가정합니다.

1. 첫 번째 프로세스는 레지스터의 값을 0으로 읽습니다.
2. 첫 번째 프로세스에서는 값에 1이 추가됩니다.카운터의 값은 1이어야 합니다만, 레지스터에의 새로운 값 기입이 완료되기 전에, 두 번째 프로세스가 실행되고 있는 동안, 카운터가 일시 정지하는 일이 있습니다.
3. 두 번째 프로세스는 레지스터의 값을 읽습니다.이것은 여전히 0과 같습니다.
4. 두 번째 프로세스는 가치에 하나를 추가합니다.
5. 두 번째 프로세스는 새로운 값을 레지스터에 쓰고 레지스터는 값 1을 가집니다.

두 번째 프로세스의 실행이 종료되고 첫 번째 프로세스가 중단된 부분부터 계속 실행됩니다.

1. 첫 번째 프로세스는 레지스터에 1을 쓰고 다른 프로세스가 레지스터의 값을 이미 1로 업데이트한 것을 알지 못합니다.

위의 예에서는 2개의 프로세스에서 increment 명령어가 호출되었지만 오브젝트의 값은 2가 아닌0에서1로 증가했을 뿐입니다.시스템이 선형화되지 않아 증분 작업 중 하나가 손실되었습니다.

위의 예는 데이터 구조의 구현을 통해 신중하게 생각할 필요성과 선형성이 시스템의 정확성에 어떤 영향을 미칠 수 있는지를 보여준다.

아토믹

선형화 가능 또는 원자 카운터 객체를 구현하기 위해 우리는 각 프로세스 Pi가 자체 레지스터 Ri를 사용하도록 이전 구현을 수정할 것입니다.

각 프로세스는 다음 알고리즘에 따라 증분 및 읽기를 수행합니다.

증가:

1. 레지스터 Ri의 값을 읽습니다.
2. 값에 1을 추가합니다.
3. 새로운 가치를 리에 다시 써넣다

읽기:

1. 레지스터 R1, R2, ...를 읽습니다.Rn.
2. 모든 레지스터의 합계를 반환합니다.

이 실장에서는, 원래의 실장으로 문제를 해결합니다.이 시스템에서는 증분 연산이 쓰기 단계에서 선형화됩니다.증분 연산의 선형화 지점은 해당 연산이 레지스터 Ri에 새 값을 쓸 때입니다.판독에 의해 반환된 값이 각 레지스터 Ri에 저장된 모든 값의 합계와 같을 경우 판독 연산은 시스템의 한 포인트로 선형화됩니다.

이것은 사소한 예시입니다.실제 시스템에서는 작업이 더 복잡해지고 오류가 매우 미묘하게 발생할 수 있습니다.예를 들어 메모리에서 64비트 값을 읽는 것은 실제로 2개의 32비트 메모리 위치에 대한 2개의 순차적 읽기로 구현될 수 있습니다.프로세스가 첫 번째 32비트만 읽고 두 번째 32비트를 읽기 전에 메모리 내의 값이 변경되면 원래 값도 새 값도 아닌 혼합 값이 됩니다.

또한 프로세스가 실행되는 특정 순서에 따라 결과가 변경될 수 있으므로 이러한 오류의 검출, 재현 및 디버깅이 어렵습니다.

비교 및 스왑

대부분의 시스템은 메모리 위치에서 읽어들이고 사용자가 제공한 "예상된" 값과 비교하며 두 값이 일치하면 "새" 값을 쓰고 업데이트가 성공했는지 여부를 반환합니다.이를 사용하여 다음과 같이 비원자 카운터 알고리즘을 수정할 수 있습니다.

1. 메모리 위치의 값을 읽습니다.
2. 1을 값에 추가한다.
3. compare-and-compare를 사용하여 증가된 값을 다시 쓴다.
4. compare-and-param에 의해 읽혀진 값이 원래 읽혀진 값과 일치하지 않는 경우 재시도합니다.

비교 및 스왑은 즉시 이루어지기 때문에(또는 발생하는 것처럼 보이기 때문에) 진행 중에 다른 프로세스가 로케이션을 갱신하면 비교 및 스왑은 실패합니다.

페치 앤 인크리먼트

많은 시스템에서는 메모리 위치에서 읽어들이고 무조건 새로운 값(이전 값+1)을 쓰고 이전 값을 반환하는 원자적인 fetch-and-increment 명령을 제공합니다.이를 사용하여 다음과 같이 비원자 카운터 알고리즘을 수정할 수 있습니다.

1. 이전 값을 읽고 증가된 값을 다시 쓰려면 fetch-and-increment를 사용합니다.

Fetch-and-Increment를 사용하는 것은 비교 ^[5]및 스왑보다 항상 더 나은(메모리 참조를 적게 필요로 하는) 알고리즘입니다.단, Herlihy는 이전에 Fetch-and-Increment만 사용하여 구현할 수 없는 특정 알고리즘에 비교 및 스왑이 더 낫다는 것을 증명했습니다.따라서 fetch-and-increment와 compare-and-swap(또는 동등한 명령)을 모두 갖춘 CPU 설계는 둘 ^[5]중 하나만 있는 CPU 설계보다 더 나은 선택이 될 수 있습니다.

잠금

또 다른 접근법은 잠금을 사용하여 Naigive 알고리즘을 중요한 섹션으로 전환하여 다른 스레드의 중단을 방지하는 것입니다.다시 비원자 카운터 알고리즘을 수정합니다.

1. 다른 나사산이 크리티컬 섹션을 동시에 실행하는 것을 제외하고 잠금을 획득합니다(2-4단계).
2. 메모리 위치의 값을 읽습니다.
3. 1을 값에 추가한다.
4. 증가된 값을 메모리 위치에 다시 쓴다.
5. 자물쇠를 열다

이 전략은 예상대로 작동합니다. 잠금 기능을 사용하면 해제될 때까지 다른 스레드가 값을 업데이트할 수 없습니다.그러나 원자 연산을 직접 사용하는 것과 비교하면 잠금 경합으로 인해 상당한 오버헤드가 발생할 수 있습니다.따라서 프로그램 성능을 향상시키기 위해 논블로킹 동기화를 위한 원자적인 조작으로 단순한 크리티컬 섹션을 대체하는 것이 좋은 생각일 수 있습니다(우리가 방금 카운터에 대해 비교 및 스왑과 fetch-and-increment를 사용한 것과 같이). 그러나 유감스럽게도 상당한 개선은 보장되지 않고 lock-fre입니다.e알고리즘은 너무 복잡해지기 쉬우므로 노력할 가치가 없다.

「 」를 참조해 주세요.

• 원자 트랜잭션
• 일관성 모델
• 산성의
• Read-Copy-Update(RCU)
• 읽기, 변경, 쓰기
• 사용시간 확인

레퍼런스

추가 정보

• Herlihy, Maurice P.; Wing, Jeannette M. (1987). Axioms for Concurrent Objects. Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '87. p. 13. doi:10.1145/41625.41627. ISBN 978-0-89791-215-0. S2CID 16017451.
• Herlihy, Maurice P. (1990). A Methodology for Implementing Highly Concurrent Data Structures. ACM SIGPLAN Notices. Vol. 25. pp. 197–206. CiteSeerX 10.1.1.186.6400. doi:10.1145/99164.99185. ISBN 978-0-89791-350-8.
• Herlihy, Maurice P.; Wing, Jeannette M. (1990). "Linearizability: A Correctness Condition for Concurrent Objects". ACM Transactions on Programming Languages and Systems. 12 (3): 463–492. CiteSeerX 10.1.1.142.5315. doi:10.1145/78969.78972. S2CID 228785.
• Aphyr. "Strong Consistency Models". aphyr.com. Aphyr. Retrieved 13 April 2018.