간섭의 자유

Interference freedom

컴퓨터 과학에서 간섭 자유는 공유 변수를 가진 동시 프로그램의 부분적 정확성을 증명하는 기술이다.Hoare 로직은 순차적 프로그램의 정확성을 증명하기 위해 앞서 도입되었다.Susan Owicki는 어드바이저 David Gries의 박사학위[1] 논문(및 이에 따른 논문)에서 이 작업을 동시 프로그램에 적용하기 위해 확장했습니다.

동시 프로그래밍은 1960년대 중반부터 운영 체제를 동시 프로세스 집합으로 코딩하기 위해 사용되었지만(특히 Dijkstra 참조), 정확성을 입증하는 공식적인 메커니즘은 없었다.[4]개별 프로세스의 인터리빙 실행 시퀀스에 대한 추론은 어렵고 오류가 발생하기 쉬우며 확장되지 않았습니다.간섭 자유는 실행 시퀀스가 아닌 증명에 적용됩니다.한 프로세스의 실행이 다른 프로세스의 정확성 증명에 간섭할 수 없음을 보여줍니다.

간섭 자유도를 사용하여 다양한 복잡한 동시 프로그램이 올바른 것으로 입증되었으며, 간섭 자유도는 공유 변수를 사용하여 동시 프로그램을 개발하고 정확함을 증명하는 후속 작업의 많은 기초를 제공합니다.Owicki-Gries 논문 병렬 프로그램에 대한 자명한 증명 기법 나는 프로그래밍 언어와 시스템에서 [5][6]1977 ACM Award 최우수 논문을 받았다.

참고. 램포트도 비슷한 생각을 하고 있어.「이 논문의 초판을 쓰고 나서, 오위키의 [1][2]근작을 알게 되었다」라고 쓰고 있다.그의 논문은 if 문이나 while loop과 같은 프로그래밍 구조 텍스트 대신 흐름도를 사용했기 때문에 Owicki-Gries만큼 주목을 받지 못했습니다.Lamport는 Floyd의 방법을 일반화하고 Owicki-Gries는 Hoare의 [9]방법을 일반화하고 있었습니다.기본적으로 이 영역의 이후의 모든 작업은 흐름도가 아닌 텍스트를 사용합니다.보조 변수에 대한 섹션에서 또 다른 차이점에 대해 설명합니다.

데이크스트라의 비간섭 원리

Edsger W. Dijkstra는 [10]1965년에 작성된 EWD 117의 비간섭 원리를 소개하였다.이 원칙은 다음과 같습니다.부품의 내부 구조가 아닌 외부 사양(전체 사양 생략)만을 고려하여 전체의 정확성을 확인할 수 있습니다.Dijkstra는 이 원리를 사용하는 일반적인 단계를 개략적으로 설명했습니다.

  1. 각 개별 부품의 완전한 사양을 제공합니다.
  2. 사양에 맞는 프로그램 부품을 구할 수 있을 때 전체적인 문제가 해결되었는지 확인합니다.
  3. 개별 부품은 사양을 만족시키되, 서로 독립적으로 구성하며 사용할 컨텍스트에 의존하지 않습니다.

그는 프로그래밍 외에 이 원리의 몇 가지 예를 들었다.그러나 프로그래밍에서 그것의 사용이 주요 관심사이다.예를 들어, 메서드(서브루틴, 함수 등)를 사용하는 프로그래머는, 그 실행이 아니고, 그 동작과 호출 방법을 결정하기 위해서, 그 사양에만 의존할 필요가 있습니다.

프로그램 사양은 Tony Hoare [9]경에 의해 소개된 Hoare 로직으로 작성되며, 공정 S1과 S2의 사양에 예시되어 있다.

{pre-S1} {pre-S2}
S1 S2
{post-S1} {pre-S2}

의미:전제조건 pre-Si가 true인 상태에서 si의 실행이 종료되면 종료 시 post-Si가 true이다.

이제 공유 변수를 사용한 동시 프로그래밍을 고려해 보겠습니다.2개(또는 그 이상) 공정 S1과 S2의 사양은 그 전후의 조건으로 제시되며, S1과 S2의 사양에 맞는 실장이 제시된다고 가정한다.그러나 이들 구현이 동시에 실행되면 변수를 공유하기 때문에 레이스 조건이 발생할 수 있습니다.한 프로세스는 공유 변수를 다른 프로세스의 증명에서 예상하지 못한 값으로 변경하기 때문에 다른 프로세스는 의도한 대로 작동하지 않습니다.

따라서 Dijkstra의 비간섭 원칙은 위반된다.

1975년 코넬 대학교 컴퓨터 과학 박사학위 논문(고문 데이비드 그리즈 아래 작성)에서 수잔 오위키는 간섭 자유 개념을 개발했습니다.프로세스 S1과 S2가 간섭의 자유도를 만족시키면 병렬 실행은 계획대로 동작한다.Dijkstra는 이 작업을 Hoare 논리를 동시 [11]프로세스에 적용하기 위한 첫 번째 중요한 단계라고 불렀습니다.논의를 간소화하기 위해 Owicki-Gries는[2][3] 더 많은 프로세스를 허용하지만, 두 프로세스만 동시에 처리하도록 제한합니다.

증명 개요에 관한 간섭의 자유도

Owicki-Gries는[2][3] Hoare 트리플 {P}S{Q}의 검증 개요를 발표했습니다.Hoare 논리의 공리와 추론 규칙을 사용하여 {P}S{Q}의 정확성을 증명하는 데 필요한 모든 세부 정보가 포함되어 있습니다.(이 작업에서는 할당문 x:= e, if-then 및 if-then-then-time 문 및 while 루프를 사용합니다.)Hoare는 그의 초기 작품에서 증명된 윤곽을 암시했다; 간섭의 자유를 위해, 그것은 공식화되어야만 했다.

{P}S{Q}에 대한 증명 개요는 사전 조건 P로 시작하여 사후 조건 Q로 끝납니다.중괄호 { 및 } 내의 두 개의 어설션이 서로 옆에 나타나면 첫 번째 어설션이 두 번째 어설션을 의미해야 합니다.

예: {P} S {Q}에 대한 증명 개요입니다. 여기서 S는 다음과 같습니다.
x:= a. e이면 S1이고, 그렇지 않으면 S2

{P}
{P1[x/a]}
x:= a;
{P1}
e일 경우 {P1 e e}
S1
{Q1}
그렇지 않으면 {P1 ∧}e}
S2
{Q1}
{Q1}
{Q}

P p P1 [ x / a ]유지해야 합니다.여기서 P1 [ x / a ]는 x가 a로 대체될 때마다 P1을 나타냅니다.(이 예에서 S1 및 S2는 할당문, 건너뛰기문, 대기문 등 기본적인 문입니다.)

증명 개요의 각 스테이트먼트 T는 전제 조건 pre-T와 post-T로 이어지며, {pre-T}T{post-T}는 Hoare 로직의 몇 가지 공리 또는 추론 규칙을 사용하여 증명 가능해야 합니다.따라서 증명 개요에는 {P}S{Q}이(가) 올바른지 확인하는 데 필요한 모든 정보가 포함되어 있습니다.

이제 병렬로 실행되는 두 개의 프로세스 S1과 S2와 그 사양에 대해 생각해 보겠습니다.

{pre-S1} {pre-S2}
S1 S2
{post-S1} {post-S2}

적절하게 병렬로 작동함을 증명하려면 다음과 같이 제한해야 합니다.S1 또는 S2의 각 식 E는 E가 평가되는 동안 다른 프로세스에 의해 변경될 수 있는 변수 y를 최대 1개까지 참조할 수 있으며, E는 최대 1회 y를 참조할 수 있다.할당문 x:= E에도 유사한 제한이 적용됩니다.

이 규칙에서는 분리할 수 없는 유일한 동작은 메모리 참조가 필요합니다.예를 들어, 공정 S1이 변수 y를 참조하는 반면 S2는 y를 변경한다고 가정합니다.S1이 y에 대해 수신하는 값은 S2가 y를 변경하기 전후의 값이어야 하며, 그 사이에 일부 가짜 값이 있어서는 안 된다.

간섭 없는 정의

Owicki-Gries의 중요한 혁신은 문장 T가 {P}S{Q}의 증명을 방해하지 않는 것이 무엇을 의미하는지 정의하는 것이었다.T의 실행이 {P}S{Q}의 증명 개요에 제시된 주장을 위조할 수 없는 경우, S와 T의 동시 실행에도 그 증명은 유지됩니다.

정의.사전 조건이 T인 스테이트먼트 T는 다음 두 조건이 유지되는 경우 {P}S{Q}의 증명을 방해하지 않습니다.

(1) {Q † 프리 T} T {Q}
(2) S'는 S' 내의 임의의 스테이트먼트이지만 wait 스테이트먼트(후술 섹션 참조) 내의 스테이트먼트라고 한다.다음으로 {pre-S' pre pre-T} T {pre-S'}입니다.

마지막 Hoare 트리플을 이렇게 읽어보세요.T'와 S'를 모두 실행할 수 있는 상태라면 T의 실행은 S'를 조작하지 않는다.

정의.다음 조건이 충족되면 {P1}S1{Q1} 및 {P2}S2{Q2}에 대한 증명 개요에 간섭이 없습니다.T를 공정 S1의 대기문 또는 할당문(대기문에는 나타나지 않음)으로 합니다.그러면 T가 {P2}S2{Q2}의 증명을 방해하지 않습니다.프로세스 S2 및 {P1}S1{Q1}의 T도 이와 유사합니다.

스테이트먼트는 공동 시작 및 대기

동시성을 다루기 위해 두 개의 진술이 도입되었다.스테이트먼트 cobegin S1 // S2 코엔드는 S1과 S2를 병렬로 실행한다.S1과 S2가 모두 종료되었을 때 종료됩니다.

wait 스테이트먼트의 실행은 B를 기다리고, 그 후 조건 B가 true가 될 때까지 S가 지연된다.다음으로 스테이트먼트 S는 분할할 수 없는 액션으로서 실행됩니다.B의 평가는 분할할 수 없는 액션의 일부입니다.2개의 프로세스가 같은 조건 B를 기다리고 있는 경우, 그것이 true가 되었을 때, 한쪽 프로세스가 계속 대기하고 다른 한쪽 프로세스가 계속 진행됩니다.

wait 문은 효율적으로 구현할 수 없으며 프로그래밍 언어에 삽입할 것을 제안하지 않습니다.대신 세마포어와 같은 몇 가지 표준 기본 요소를 나타내는 수단을 제공합니다. 먼저 세마포 연산을 기다리는 대로 표현한 다음 여기에 설명된 기술을 적용합니다.

wait 및 cobegin에 대한 추론 규칙은 다음과 같습니다.

기다리다
{P b B} S {Q}/{P}이(가) B를 기다린 후 S {Q}

시작되다
{P1} S1 {Q1}, {P2} S2 {Q2}
간섭이 없는/{P1pP2} 코비긴 S1//S2 코엔드 {Q1qQ2}

보조 변수

보조 변수는 프로그램에서 발생하지 않지만 추론을 단순하게 하기 위해 정확성을 입증하는 과정에서 도입됩니다.보조변수는 보조변수에 대한 할당에서만 사용되므로 입력에 대한 프로그램 변경이나 프로그램 변수 값에 영향을 주지 않습니다.일반적으로 프로그램 카운터 또는 계산 이력을 기록하는 데 사용됩니다.

정의.AV를 할당 x:= E에서만 S'에 나타나는 변수 집합으로 합니다. 여기서 x는 AV에 있습니다.그러면 AV는 S'에 대한 보조 변수 집합입니다.

보조 변수의 집합 AV는 AV의 변수에 대한 할당에서만 사용되므로, AV에 대한 할당을 모두 삭제해도 프로그램의 정확성은 변경되지 않으며, 추론 규칙 AV가 제거됩니다.

{P} S' {Q}/{P} S {Q}

AV는 S'에 대해 설정된 보조 변수입니다.AV의 변수는 P나 Q'에서 발생하지 않으며, AV의 변수에 대한 모든 할당을 삭제하여 S'에서 얻는다.

보조 변수를 사용하는 대신 프로그램 카운터를 프루프 시스템에 도입할 수 있지만, 프루프 시스템에 복잡성을 더한다.

주의: Apt는 재귀적 어설션, 즉 효과적으로 계산 가능한 어설션의 맥락에서 Owicki-Gries 논리를 논한다.그는 증명 개요의 모든 어설션이 재귀적일 수 있다는 것을 증명한다.그러나 보조변수가 연산 이력을 기록하지 않고 프로그램 카운터로만 사용된다면 이는 더 이상 해당되지 않는다는 것을 증명 개요의 모든 어설션이 재귀적일 수 있다.Lamport는 유사한 [7]작업에서 보조 변수 대신 토큰 위치에 대한 어사션을 사용합니다. 여기서 흐름도의 가장자리에 있는 토큰은 프로그램 카운터와 유사합니다.이력 변수의 개념은 없습니다.이는 Owicki-Gries와 Lamport의 접근방식이 재귀적 어설션으로 제한될 경우 동등하지 않음을 나타냅니다.

교착 상태 및 종료

Owicki-Gries는[2][3] 주로 부분적인 정확성에 대해 다룹니다.{ P } S {Q }는 P가 참인 상태에서 실행된 S가 종료되면 Q는 종료 시 상태에 대해 참입니다.그러나 Owicki-Gries는 교착 상태, 프로그램 종료 및 상호 배제를 포함한 다른 정확성 특성을 도출하기 위해 부분적 정확성 증명에서 얻은 정보를 사용하는 몇 가지 실용적인 기법도 제공한다.

종료되지 않은 모든 프로세스가 wait 문을 실행하고 대기 조건이 false이기 때문에 진행할 수 없는 경우 프로그램은 교착 상태가 됩니다.Owicki-Gries는 교착 상태가 발생하지 않는 조건을 제공합니다.

Owicki-Gries는 while 루프의 완전 수정에 대한 추론 규칙을 제시합니다.반복할 때마다 감소하는 바운드 함수를 사용하며 루프 조건이 참인 한 양수입니다.Apt 등은 이 새로운 추론 규칙이 간섭의 자유를 만족시키지 못한다는 것을 보여준다.루프 조건이 참인 한 결합 함수가 양수라는 사실은 간섭 테스트에 포함되지 않았습니다.그들은 이 실수를 바로잡는 두 가지 방법을 보여준다.

간단한 예

다음 문장을 고려합니다.
{x=0}
cobegin은 true를 기다린 후 x:= x+1
// 참을 기다린 후 x:= x+2
코인드
{x=3}

그 실증 개요:

{x=0}
S: cobegin
{x=0}
{x=0 † x=2}
S1: 그럼 참을 기다린다.x:=x+1
{Q1: x=1 † x=3}
//
{x=0}
{x=0 ∨ xx=1}
S2: 참이 되기를 기다리다x:=x+2
{Q2: x=2 † x=3}
코인드
{(x=1 ∨ x=3) ∧ (x=2 ∨ x=3)}
{x=3}

S1이 S2의 증명을 방해하지 않는다는 것을 증명하려면 두 개의 호어 트리플을 증명해야 한다.

(1) {(x=0 ∨ x=2) ( (x=0 x x=1} S1 {x=0 x x=1}
(2) {(x=0 ∨ x=2) ( (x=2 x x=3) S1 {x=2 x x=3}

(1)의 전제조건은 x=0으로 감소하고 (2)의 전제조건은 x=2로 감소한다.이것으로부터, 이 호아레 트리플들이 버티고 있다는 것을 쉽게 알 수 있다.S2가 S1의 증명을 방해하지 않는다는 것을 보여주기 위해 두 개의 유사한 호어 트리플이 필요하다.

S1이 wait 문에서 할당 x:= x+1로 변경되었다고 가정합니다.그러면 할당에 공유 변수 x가 두 개 포함되어 있기 때문에 증명 개요가 요구 사항을 충족하지 못합니다.실제로 cobegin 스테이트먼트의 실행 후의 x 값은 2 또는 3이 될 수 있습니다.

만약 S1이 wait true이고 그 다음 x:= x+2이므로 S2와 같다.S 실행 후 x는 4가 됩니다.이를 증명하기 위해서는 두 개의 할당이 동일하기 때문에 S1의 실행 여부를 나타내는 변수와 S2의 실행 여부를 나타내는 변수 두 개가 필요하다.증명 개요의 변경은 독자에게 맡깁니다.

공식적으로 입증된 동시 프로그램의 예

A. Findpos.배열의 첫 번째 양의 요소를 찾는 프로그램을 작성합니다(있는 경우).한 프로세스는 어레이의 짝수 위치에서 모든 어레이 요소를 검사하고 양의 값을 찾거나 아무것도 찾지 못하면 종료됩니다.마찬가지로 다른 프로세스도 배열의 홀수 위치에서 배열 요소를 확인합니다.따라서 이 예에서는 while loops에 대해 설명합니다.또한 대기 문구가 없습니다.

이 예는 Barry K에서 가져온 것입니다.로젠,[14] 오위키 [2]그리스의 해법은 프로그램, 입증 개요, 간섭 자유에 대한 논의까지 포함하면 2페이지도 안 걸려요공유 변수는 1개뿐이므로 간섭 자유도를 확인하는 것은 매우 쉽습니다.이와는 대조적으로 로젠의 기사에서는[14] 이 24페이지 분량의 논문에서 Findpos를 하나의 실행 예시로 사용하고 있습니다.

일반적인 환경에서의 두 프로세스의 개요:

cobegin 프로듀서: ...
입력 대기 < N 후 건너뜁니다.
추가: b[mod N]:= 다음 값;
마크인:인:=입력+1;
...
//
개인 사용자: ...
in-out > 0을 기다린 후 건너뜁니다.
삭제:이 값:=
b[out mod N];
마크아웃:출력:=출력+1;
코인드
...

B. 버퍼 소비자/생산자 제한 문제.생산자 프로세스는 값을 생성하여 크기 N의 경계 버퍼 b에 넣고, 소비자 프로세스에 의해 값을 제거한다.그들은 변동 환율로 진행됩니다.버퍼 b가 가득 차면 생산자는 대기하고 버퍼 b가 비어 있으면 소비자는 대기해야 합니다.Owicki-Gries에서는 [2]일반적인 환경에서의 솔루션이 제시되어 있습니다.그 후 어레이 c[1]를 복사하는 프로그램에 포함되어 있습니다.M]을 배열 d[1]로 변환합니다.M]

다음 예에서는 간섭 체크를 최소한으로 줄이는 원리를 보여 줍니다.두 프로세스 모두에서 항상 맞는 주장을 가능한 많이 배치합니다.이 경우, 어설션은 버퍼에 추가 및 삭제되는 값의 수를 나타내는 바운드의 정의와 변수의 경계입니다.버퍼 b 자체 외에 2개의 공유 변수가 버퍼에 추가된 값의 수와 버퍼에서 삭제된 값을 기록합니다.

C. 세마포어 구현Dijkstra는 THE 멀티프로그래밍 [4]시스템에 관한 기사에서 세마포 sem을 동기화 프리미티브로 소개하고 있습니다.sem은 다음과 같이 두 가지 방법으로만 참조할 수 있는 정수 변수이며, 각각은 분할할 수 없는 연산입니다.

1. P(sem):sem을 1 줄인다.sem < 0인 경우 프로세스를 일시정지하고 sem과 관련된 일시정지 프로세스 목록에 추가합니다.

2. V(sem):sem을 1씩 늘립니다.현재 sem ,0인 경우 sem과 관련된 일시정지된 프로세스 목록에서 프로세스 중 하나를 삭제하여 동적 진행이 다시 허용되도록 합니다.

wait 문을 사용한 P 및 V의 구현은 다음과 같습니다.

P(sem):
기다리다 진실의 그리고나서
시작 sem:=sem-1;
sem < 0인 경우
ww[이 프로세스]:= 진실의
종료.
이 과정을 기다리다[이] 기다리다
그리고나서 건너뛰다.

V(sem):
기다리다 진실의 그리고나서
시작 sem:=sem+1;
sem then 0이면
그런 것을 고르기 시작하다
w[p];
w[p]:= 거짓의
끝.
끝.

여기서 w는 일시정지되어 대기 중인 프로세스의 배열입니다.처음에는 모든 프로세스 p에 대해 w[p]=false입니다.실장을 변경하여 가장 긴 정지 프로세스를 항상 웨이크업할 수 있습니다.

D. 즉석 쓰레기 수거.1975년 여름학교 Marktoberdorf에서 Dijkstra는 병렬화를 이해하기 위한 연습으로 즉석 쓰레기 수집기에 대해 논의했다.기존 LISP 구현에서 사용되는 데이터 구조는 각 노드에 최대 2개의 발신 에지가 있는 방향 그래프이며, 이 중 하나가 누락될 수 있습니다. 즉, 발신 좌측 에지 및 발신 우측 에지입니다.그래프의 모든 노드는 알려진 루트에서 도달할 수 있어야 합니다.노드를 변경하면 노드가 도달할 수 없게 되어 더 이상 사용할 수 없게 되어 가비지라고 불립니다.온 더 플라이 가비지 콜렉터에는 프로그램 자체와 가비지 콜렉터의 두 가지 프로세스가 있습니다.이 두 가지 프로세스는 가비지 노드를 식별하고 다시 사용할 수 있도록 이들을 빈 목록에 추가하는 것입니다.

Gries는 간섭의 자유도가 온 더 플라이 가비지 컬렉터가 올바른 것을 증명하기 위해 사용될 수 있다고 생각했습니다.Dijkstra와 Hoare의 도움으로 그는 Summer School의 마지막에 프레젠테이션을 할 수 있었고, 그 결과 CACM에 [15]기사가 실렸다.

E. 세마포에 의한 리더/라이터 솔루션 검증Courtois 등은[16] 세마포어를 사용하여 두 가지 버전의 독자/작가 문제를 증명 없이 제시합니다.쓰기 작업은 읽기와 쓰기를 모두 차단하지만 읽기 작업은 병렬로 발생할 수 있습니다.오위키는[17] 증거를 제공한다.

F. Peterson's algorithm, 2-process 상호 배제 문제에 대한 해법은 Peterson에 의해 2페이지 분량의 [18]기사로 발표되었습니다.Schneider와 Andrews는 정확성의 [19]증거를 제공한다.

간섭 자유도에 대한 의존성

아래 그림은 Ilya Sergey가 동시성을 다루는 논리로 구현한 아이디어의 흐름을 나타낸 것입니다.근본은 간섭의 자유입니다.파일CSL-Family-Tree (PDF) 에 레퍼런스를 나타냅니다.이하에 주요 진보를 정리합니다.

Historical graph of program logics for interference freedom
  • 신뢰 보증.1981년, 간섭의 자유는 구성적인 것이 아닙니다.Cliff[20][21] Jones는 간섭을 사양의 두 가지 새로운 술어로 추상화함으로써 합성성을 회복합니다.즉, 의존 조건은 스레드가 허용할 수 있는 간섭을 기록하고 보증 조건은 스레드가 형제 스레드에 가할 수 있는 간섭의 상한을 설정합니다.Shu 등은 Relate-Garantee가 간섭 자유도를 재구성한 것이라고 관찰했다.이 두 방법 간의 연관성을 밝히는 것은 공유 변수 프로그램의 검증에 대한 깊은 이해를 제공한다고 한다.
  • CSL. 2004.분리 로직은 프로그램 컴포넌트의 사양 및 증명이 컴포넌트에 의해 사용되는 메모리의 일부만을 언급하는 로컬 추론을 지원한다.CSL(Concurrent separation logic)은 [23][24]원래 Peter O'Hearn에 의해 제안되었으며, "Owicki-Gries 방법은[2] 프로그램 컴포넌트 간의 비간섭에 대한 명시적인 체크를 포함하며, 우리의 시스템은 암묵적인 방식으로 간섭을 배제합니다."라고 우리는 [23]인용합니다.
  • 동시 프로그램 유도.2005-2007.Feijen과 van Gasteren은[25] Owicki-Gries를 사용하여 동시 프로그램을 설계하는 방법을 보여주고 있지만, 진행 이론이 없다는 것은 설계가 안전 요건에 의해서만 추진된다는 것을 의미한다.Dongol, Goldson, Moij 및 Hayes는 이 작업을 Chandy와 Misra의 언어 Unity에 기초한 "진보의 논리"를 포함하도록 확장하여 순차 프로그래밍 모델에 맞게 성형했습니다.Dongel과[26] Goldson은 그들의 진보 논리를 설명한다.Goldson과 Dongol은[27] 두 가지 프로세스에 대한 Dekker 알고리즘을 예로 들어 이 논리가 프로그램 설계 프로세스를 개선하는 데 어떻게 사용되는지 보여줍니다.Dongol과[28] Moij는 Peterson의 상호 배제 알고리즘을 예로 들어 프로그램을 도출하는 더 많은 기술을 제시한다.Dongol과 Moij는[29] 공식 증명과 도출에서 계산 오버헤드를 줄이고 Dekker의 알고리즘을 다시 도출하는 방법을 보여 주며, 이는 알고리즘의 새롭고 단순한 변형을 이끌어낸다.Moij는[30] Unity의 유도 관계에 대한 계산 규칙을 연구합니다.마지막으로 Dongol과[31] Hayes는 프로세스 로직의 건전성을 증명하는 이론적 근거를 제공한다.
  • OGRA 2015년Lahav와 Vafeiadis는 간섭 자유도 검사를 강화하여 (추상으로부터 인용한다) "OGRA, C11 메모리 모델의 릴리스-취득 단편에서 프로그램에 대한 추론에 적합한 프로그램 논리"를 생성한다.RCU 동기 프리미티브의 [32]실장 등, 그 사용 예를 몇개인가 나타냅니다.
  • 양자 프로그래밍. 2108.Ying 등은 간섭의 자유를 양자 프로그래밍으로 확장했다.그들이 직면하는 어려움은 양자 측정을 수반하는 비결정론과 동시에 일어나는 병렬에 의해 도입된 비결정론이라는 얽힌 비결정론이다.저자들은 선형 대수 문제를 푸는 브라비-고셋-쾨니그의 병렬 양자 알고리즘을 공식적으로 검증하고, 그들은 처음으로 계산 양자 우위성의 무조건적인 증거를 제공한다고 말한다.
  • 2020년 포그Raad 등에서는, 비휘발성 메모리 테크놀로지, 특히 Intel-x86에 [34]관한 최초의 프로그램 로직인 POG(Persistent Owicki-Gries)를 소개합니다.

간섭 자유에 대해 설명하는 텍스트

  • 멀티프로그래밍 방법론, 1999.[25]Van Gasteren과 Feijen은 완전히 간섭 자유라는 개념에 기초하여 동시 프로그램의 공식적인 개발에 대해 논의합니다.
  • Current Programming, 1997.[35]Schneider는 동시 프로그램을 개발하고 증명하는 주요 도구로 간섭 자유도를 사용합니다.시간논리에 대한 연결이 주어지기 때문에 임의의 안전성과 생존성을 증명할 수 있다.제어 술어는 프로그램 카운터에 대한 추론을 위한 보조 변수의 필요성을 배제합니다.
  • 순차 및 동시 프로그램 검증, 1991,[36] 2009.[37]Apt 등에 의한 구조화된 동시 프로그램의 검증을 다루는 이 첫 번째 텍스트는 수십 년에 걸쳐 여러 판을 거쳤다.
  • 동시성 검증: 구성 및 비구성 방법 입문, 2112.[38]De Roever 등은 동시 프로그램의 국가 기반 검증을 위한 구성 및 비구성 증명 방법에 대한 체계적이고 포괄적인 소개를 제공한다.

간섭 자유 구현

  • 1999: Nipkow와 Nieto는 간섭 자유 및 그 구성 버전인 의존 보증 방법의 첫 번째 공식화를 정리 프로버로 제시한다.이사벨/[39][40]홀
  • 2005년 : Abraham 박사논문에서는 멀티스레드 Java 프로그램이 올바른지 검증할 수 있는 방법이 3단계로 제시되어 있습니다. (1) 검증 개요를 작성하기 위한 프로그램 주석 작성, (2) 검증 조건을 자동으로 작성하기 위한 도구 Verger 사용, (3) 검증 조건을 인터랙티브하게 [41][42]증명하기 위한 정리 프로버 PVS 사용.
  • 2017년[43]: Denissen은 Owicki-Gries의 실장에 대해 "검증 [44]준비 완료" 프로그래밍 언어 Dafny로 보고합니다.데니센은 Dafny의 사용 편의성과 그 확장에 대해 언급하고 있어 학생들에게 간섭의 자유에 대해 가르칠 때 매우 적합하다.그것의 단순함과 직관성은 비구성의 단점보다 더 중요하다.그는 간섭의 자유를 가르치는 20여 개의 기관을 열거했다.
  • 2017년 : Amani 등 연구진은 간단한 언어를 위해 이사벨/HOL의 Owicki-Gries를 공식화한 Hoare-Parallel과 이사벨/HOL에 내장된 범용 언어 SIMPLE의 접근방식을 결합하여 C [45]프로그램에 대한 공식적인 추론을 가능하게 했다.
  • 2022년: Dalvandi 등은 C11과 같은 약한 기억 프로그램을 위한 이자벨/HOL의 첫 연역적 검증 환경을 도입하고, Nipkow와 Nieto의 이자벨 정리프로버에서의 [46]Owicki-Gries 부호화를 기반으로 한다.
  • 2022: 이 웹 페이지에서는 동시 프로그램용 Civl Verifier에 대해 설명하고 컴퓨터에 설치하는 방법에 대해 설명합니다.그것은 연속 프로그램의 검증자인 Boogie 위에 만들어졌다.Kragl 등은 Civl에서 간섭 자유도가 어떻게 달성되는지를 그들의 새로운 규격 관용어인 수율 불변수를 사용하여 설명한다.사양은 의존보증 방식으로도 사용할 수 있다.Civl은 분리 로직과 같은 분리에 대한 경제적이고 국지적인 추론을 가능하게 하는 선형 타이핑과 논리의 조합을 제공합니다.Civl은 구조화된 동시 프로그램에 대한 정교한 추론을 제공하는 첫 번째 시스템입니다.
  • 2022. Esen과 Rümer는 C 프로그램용 자동 오픈 소스 검증 도구인 TRICERA를 [49]개발하였습니다.이것은 구속된 Horn 절의 개념을 기반으로 하며 힙 이론을 사용하여 힙에서 작동하는 프로그램을 처리합니다.온라인으로 시험할 수 있는 웹 인터페이스를 이용할 수 있습니다.동시성을 처리하기 위해 TRICERA는 Owicki-Gries 증명 규칙의 변형을 사용하고 시간과 클럭을 나타내기 위해 명시적 변수를 추가합니다.

레퍼런스

  1. ^ a b c Owicki, Susan S. (August 1975). Axiomatic Proof Techniques for Parallel Programs (PhD thesis). Cornell University. hdl:1813/6393. Retrieved 2022-07-01.
  2. ^ a b c d e f g h i Owicki, Susan; Gries, David (25 June 1976). "An axiomatic proof technique for parallel programs I". Acta Informatica. Berlin: Springer (Germany). 6 (4): 319–340. doi:10.1007/BF00268134. S2CID 206773583.
  3. ^ a b c d Owicki, Susan; Gries, David (May 1976). "Verifying properties of parallel programs: an axiomatic approach". Communications of the ACM. 19 (5): 279–285. doi:10.1145/360051.360224. S2CID 9099351.
  4. ^ a b Dijkstra, E.W. (1968), "The structure of the 'THE'-multiprogramming system", Communications of the ACM, 11 (5): 341–346, doi:10.1145/363095.363143, S2CID 2021311
  5. ^ "Susan S Owicki". Awards.acm.org. Retrieved 2022-07-01.
  6. ^ "David Gries". Awards.acm.org. Retrieved 2022-07-01.
  7. ^ a b Lamport, Leslie (March 1977). "Proving the correctness of multiprocess programs". IEEE Transactions on Software Engineering. SE-3 (2): 125–143. doi:10.1109/TSE.1977.229904. S2CID 9985552.
  8. ^ Floyd, Robert W. (1967). "Assigning Meanings to Programs" (PDF). In Schwartz, J.T. (ed.). Mathematical Aspects of Computer Science. Proceedings of Symposium on Applied Mathematics. Vol. 19. American Mathematical Society. pp. 19–32. ISBN 0821867288.
  9. ^ a b Hoare, C. A. R. (October 1969). "An axiomatic basis for computer programming". Communications of the ACM. 12 (10): 576–580. doi:10.1145/363235.363259. S2CID 207726175.
  10. ^ "Programming Considered as a Human Activity" (PDF). E. W. Dijkstra Archive. University of Texas.
  11. ^ Dijkstra, Edsger W. (1982). "EWD 554: A personal summary of the Gries-Owicki Theory". Selected Writings on Computing: A Personal Perspective. Monographs in Computer Science. Springer-Verlag. pp. 188–199. ISBN 0387906525.
  12. ^ Apt, Krzysztof R. (June 1981). "Recursive assertions and parallel programs". Acta Informatica. 15 (3): 219–232. doi:10.1007/BF00289262. S2CID 42470032.
  13. ^ Apt, Krzysztof R.; de Boer, Frank S.; Olderog, Ernst-Rüdiger (1990). "Proving termination of parallel programs". In Gries, D.; Feijen, W.H.J.; van Gasteren, A.J.M.; Misra, J. (eds.). Beauty is Our Business. Monographs in Computer Science. New York: Springer Verlag. pp. 0–6. doi:10.1007/978-1-4612-4476-9. ISBN 978-1-4612-8792-6. S2CID 24379938.
  14. ^ a b Rosen, Barry K (1976). "Correctness of parallel programs: The Church-Rosser Approach". Theoretical Computer Science. 2 (2): 183–207. doi:10.1016/0304-3975(76)90032-3.
  15. ^ Gries, David (December 1977). "An exercise in proving parallel programs correct". Communications of the ACM. 20 (12): 921–930. doi:10.1145/359897.359903. S2CID 3202388.
  16. ^ Courtois, P.J.; Heymans, F.; Parnas, D.L. (October 1971). "Concurrent control with "readers" and "writers"". Communications of the ACM. 14 (10): 667–668. doi:10.1145/362759.362813. S2CID 7540747.
  17. ^ Owicki, Susan (August 1977). Verifying concurrent programs with shared data classes (PDF) (Technical report). Digital Systems Laboratory, Stanford University. 147. Retrieved 2022-07-08.
  18. ^ Peterson, Gary L. (June 1981). "Myths about the mutual exclusion problem". IPL. 12 (3): 115–116. doi:10.1016/0020-0190(81)90106-X.
  19. ^ Schneider, Fred B.; Andrews, Gregory R. (1986). "Concepts for concurrent programming". In J.W. Bakker; W.P. de Roever; G. Rozenberg (eds.). Current Trends in Concurrency. Lecture Notes in Computer Science. Vol. 224. Noordwijkerhout, the Netherlands: Springer Verlag. pp. 669–716. doi:10.1007/BFb0027049. ISBN 978-3-540-16488-3.
  20. ^ Jones, C.B. (June 1981). Development Methods for Computer Programs including a Notion of Interference (PDF) (DPhil thesis). Oxford University.
  21. ^ Jones, Cliff B. (1983). R.E.A. Mason (ed.). Specification and design of (parallel) programs. 9th IFIP World Computer Congress (Information Processing 83). North-Holland/IFIP. pp. 321–332. ISBN 0444867295.
  22. ^ Xu, Qiwen; de Roever, Willem-Paul; He, Jifeng (1997). "The Rely-Guarantee method for verifying shared variable concurrent programs". Formal Aspects of Computing. 9 (2): 149–174. doi:10.1007/BF01211617. S2CID 12148448.
  23. ^ a b O'Hearn, Peter W. (2004-09-03). "Resources, Concurrency and Local Reasoning". In P. Gardner; N. Yoshida (eds.). CONCUR 2004 -- Concurrency Theory. CONCUR 2004. London, UK: Springer Verlag Berlin, Heidelberg. pp. 49–67. doi:10.1007/b100113. ISBN 978-3-540-28644-8. Retrieved 2022-07-06.
  24. ^ O'Hearn, Peter (2007). "Resources, Concurrency and Local Reasoning" (PDF). Theoretical Computer Science. 375 (1–3): 271–307. doi:10.1016/j.tcs.2006.12.035.
  25. ^ a b Van Gasteren, A.J.M.; Feijen, W.H.J. (1999). Gries, David; Schneider, Fred B. (eds.). On A Method Of Multiprogramming. Monographs in Computer Science. Springer-Verlag New York Inc. p. 370. doi:10.1007/978-1-4757-3126-2. ISBN 978-1-4757-3126-2. S2CID 13607884.
  26. ^ Dongol, Brijesh; Goldson, Doug (2006) [January 12, 2005]. "Extending the theory of Owicki and Gries with a logic of progress". Logical Methods in Computer Science. Centre pour la Communication Scientifique Directe (CCSD). 2. arXiv:cs/0512012v3. doi:10.2168/lmcs-2(1:6)2006. S2CID 302420.
  27. ^ Goldson, Doug; Dongol, Brijesh (January 2005). "Concurrent Program Design in the Extended Theory of Owicki and Gries". In Mike Atkinson; Frank Dehne (eds.). CATS '05: Proc 2005 Australasian Symp on Theory of Computing. Vol. 41. Australian Computer Society, Inc. pp. 41–50.
  28. ^ Dongol, Brijesh; Mooij, Arjan J (July 2006). "Progress in deriving concurrent programs: emphasizing the role of stable guards". In Tarmo Uustalu (ed.). MPC'06: Proc. 8th Int. Conf. on Mathematics of Program Construction. Vol. 41. Kuressaare, Estonia: Springer Verlag, Berlin, Heidelberg. pp. 14–161. doi:10.1007/11783596_11.
  29. ^ Dongol, Brijesh; Mooij, Arjan J (2008). "Streamlining progress-based derivations of concurrent program". Formal Aspects Computing. 20 (2): 141–160. doi:10.1007/s00165-007-0037-4. S2CID 7024064.
  30. ^ Mooij, Arjan J. (November 2007). "Calculating and composing progress properties in terms of the leads-to relation". In Michael Butler; Michael G. Hinchey; María M. Larrondo-Petrie (eds.). ICFEM'07: Proc. Formal Engineering Methods 9th Int. Conf. on Formal Methods and Software Engineering. Boca Raton, Florida: Springer Verlag, Berlin, Heidelberg. pp. 366–386. ISBN 978-3540766483.
  31. ^ Dongol, Brijesh; Hayes, Ian (April 2007). Trace semantics for the Owicki-Gries theory integrated with the progress logic from UNITY (PDF) (Technical report). University of Queensland. SSE-2007-02.
  32. ^ Lahav, Ori; Vafeiadis, Viktor (2015). "Owicki-Gries reasoning for weak memory models". In Halldórsson, M.; Iwama, K.; Kobayashi, N.; Speckmann, B. (eds.). Automata, Languages, and Programming. ICALP 2015. Lecture Notes in Computer Science. ICALP 2015. Vol. 9135. Kyoto, Japan: Springer, Berlin, Heidelberg. pp. 311–323. doi:10.1007/978-3-662-47666-6_25.
  33. ^ Ying, Mingsheng; Zhou, Li; Li, Yangjia (2018). "Reasoning about Parallel Quantum Programs". arXiv:1810.11334 [cs.LO].
  34. ^ Raad, Azalea; Lahav, Ori; Vafeiadis, Viktor (13 November 2020). "Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86". Proceedings of the ACM on Programming Languages. Vol. 4. ACM. pp. 1–28. doi:10.1145/3428219.
  35. ^ Schneider, Fred B. (1997). Gries, David; Schneider, Fred B. (eds.). On Concurrent Programming. Graduate Texts in Computer Science. Springer-Verlag New York Inc. doi:10.1007/978-1-4612-1830-2. ISBN 978-1-4612-1830-2. S2CID 9980317.
  36. ^ Apt, Krzysztof R.; Olderog, Ernst-Rüdiger (1991). Gries, David (ed.). Verification of Sequential and Concurrent Programs. Texts in Computer Science. Springer-Verlag Germany.
  37. ^ Apt, Krzysztof R.; Boer, Frank S.; Olderog, Ernst-Rüdiger (2009). Gries, David; Schneider, Fred B. (eds.). Verification of Sequential and Concurrent Programs. Texts in Computer Science (3rd ed.). Springer-Verlag London. p. 502. Bibcode:2009vscp.book.....A. doi:10.1007/978-1-84882-745-5. ISBN 978-1-84882-744-8.
  38. ^ de Roever, Willem-Paul; de Boer, Willem-Paul; Hanneman, Ulrich; Hooman, Jozef; Lakhnech, Yassine; Poel, Mannes; Zwiers, Job (2012). Abramsky, S. (ed.). Concurrency Verification: Introduction to Compositional and Non-Compositional Methods. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press USA. p. 800. ISBN 978-0521169325.
  39. ^ Nieto, Leonor Prensa (2002-01-31). Verification of Parallel Programs with the Owicki-Gries and Rely-Guarantee Methods in Isabelle/HOL (PhD thesis). Technischen Universitaet Muenchen. p. 198. Retrieved 2022-07-05.
  40. ^ Nipkow, Tobias; Nieto, Leonor Prensa (1999-03-22). "Owicki/Gries in Isabelle/HOL". In J.P. Finance (ed.). Fundamental Approaches to Software Engineering. FASE 1999. LNCS. Vol. 1577. Springer Verlag, Berlin Heidelberg. pp. 188–203. doi:10.1007/978-3-540-49020-3_13. ISBN 978-3-540-49020-3.
  41. ^ Ábrahám, Erika (2005-01-20). An Assertional Proof System for Multithreaded Java - Theory and Tool Support (PhD thesis). Universiteit Leiden. p. 220. hdl:1887/584. ISBN 9090189084. Retrieved 2022-07-05.
  42. ^ Ábrahám, Erika; Boer, Frank, S., de; Roever, Willem-Paul, de; Martin, Steffen (2005-02-25). "An assertion-based proof system for multithreaded Java". Theoretical Computer Science. Elsevier. 331 (2–3): 251–290. doi:10.1016/j.tcs.2004.09.019.
  43. ^ Denissen, P.E.J.G (November 2017). Extending Dafny to Concurrency: Owicki-Gries style program verification for the Dafny program verifier (Masters thesis). Eindhoven University of Technology.
  44. ^ "Dafny Programming Language". Retrieved 2022-07-20.
  45. ^ Amani, S.; Andronick, J.; Bortin, M.; Lewis, C.; Rizkallah, C.; Tuong, J. (16 January 2017). Yves Bertot; Viktor Vafeiadid (eds.). COMPLX: A verification framework for concurrent imperative programs. CPP 2017: Proc 6th ACM SIGPLAN Conference on Certified Programs and Proof. Paris, France: ACM. pp. 138–150. doi:10.1145/3018610.3018627. ISBN 978-1-4503-4705-1.
  46. ^ Dalvandi, Sadegh; Dongol, Brijesh; Doherty, Simon; Wehrheim, Heike (February 2022). "Integrating Owicki–Gries for C11-Style memory models into Isabelle/HOL". Journal of Automated Reasoning. 66: 141–171. doi:10.1007/s10817-021-09610-2. S2CID 215238874.
  47. ^ "Civl: A verifier for concurrent programs". Retrieved 2022-07-22.
  48. ^ Kragl, Bernhard; Qadeer, Shaz; Henzinger, Thomas A. (2020). "Refinement for structured concurrent programs". In S. Lahiri; C. Wang (eds.). CAV 2020: Computer Aided Verification Lecture Notes in Computer Science. Vol. 12224. Springer Verlag. doi:10.1007/978-3-030-53288-8_14. ISBN 978-3-030-53288-8.
  49. ^ Esen, Zafer; Rümmer, Philipp (October 2022). "TRICERA Verifying C Programs Using the Theory of Heaps". In A. Griggio; N. Rungta (eds.). Proc. 22nd Conf. on Formal Methods in Computer-Aided Design – FMCAD 2022. TU Wien Academic Press. pp. 360–391. doi:10.34727/2022/isbn.978-3-85448-053-2_45.