client에게 paxos node 이외의 node로 위장하여 send를 하면 nb로 바꾸는 wrapper를 씌운다.
이 client의 정보는 ginv를 만족하므로, ginv를 paxos에서 가져다 쓰면 된다.
누구나 쓸 수 있는 network(physical 구현)는 resource가 필요없다.
지금 문제는 salloc에서의 변수이름의 파악이 불가능하다는 것이다.
or 대신 tc or를 정의하여 typeclass instance auto construction를 통해 or를 증명한다.
즉, 특정한 경우 or를 보면 tcor로 전환시켜 typeclass eauto를 사용하는 것
inference를 통해 input을 output으로 강제시키는 방법
두번째로 typeclass는 특정 기능의 추상화에 사용한다. 이때 Coq의 기능을 최대한 활용할 수 있다.
세번째는 본질적으로 Class는 수학적이다.
힌트 데이터베이스는 변수나 상수의 opaque 처리 등을 지시하는 선택적 가이드 역할을 한다.
eapply with _ _ _ _ 확실한건 집어넣고 불확실한것만 subgoal로 준다.
tactic -> 거시적인 상황 분별, 지시의 역할
typeclass -> 해당 상황이 유효성 및 그에 맞는 구체적인 항을 기계적으로 찾아내는 역할 (생각할 수 있는 모든 것이 instance의 구성요소가 될 수 있다. 자주 쓰이는 것은 lemma)
결국 ‘외부정보’를 어떻게 쓰느냐가 이 주제의 핵심이 된다.
또한 normalize를 쓰면 load를 expression에서 분리해낼 수 있다.
store/load에서 사용하는 정보는 언제나 base address에 대한 predicate이다.
base address의 predicate는 언제나 내부 index에 대해 no-overflow를 보장한다.
즉, base address + index에서 중요한 것은 index만의 범위 정보이다.
따라서 적당한 user의 부등식 개입의 존재가 있다면, memory 단위로 잘라서 증명을 자동화하는 것은 어렵지 않을 것이다.
non-determinism이 함수 외부에 존재할 때, 스펙 상으로 non-determinism이 존재한다고 표시하기 위해서 허상의 non-determinism을 도입한다.
스펙은 그럼 허상의 non-determinism을 따라가게 되는데, 스펙은 실제 observable return과도 보조를 맞추어야한다. 따라서 이것이 유출될 때 resolve를 통해 허상에서 일어난 일 중 실제로 일어난 일만으로 수축시킨다.
이는 온전히 허상에서 일어난 일이기 때문에 behavior적으로는 실상을 전혀 변화시키지 않는다. 단지 모듈 내부의 허상, 타겟 실상, 소스 실상을 연결하는 치밀한 invariant를 통해 module local한 증명을 완결시킬 수 있다.
paxos-ado의 경우를 생각해보자.
prepare가 true면 그에 대응되는 ado의 global state는 당연히 pull에서 true를 내뱉도록 되어있다.
prepare가 false면 그에 대응되는 ado의 global state는 true 일수도 있고 false일수도 있다. false는 상관 없지만, true는 상관있다. 이는 invariant에 or가 붙은 상황이기 때문이다(실제 invariant는 아니지만, 모든 step에서 ado와 paxos와 허상을 잇는 무언가…). 따라서 이 경우 허상을 통해 인위적으로 non-determinism을 일으켜서 실제 global한 관측을 prepare 내에서 임의로 끌어온다.
그리고 accept의 경우 실제 global한 state에 대해 경우를 나누고 target resolve를 통해 target에서도 source와 sync가 맞는 global한 state를 얻어온다. 그리고 prepare랑 마찬가지로 new prophecy를 통해 종료 시의 invariant를 만족시킨다.
prophecy가 필요한 이유는 linearization point가 코드 외부에 존재하기 때문이다.
paxos-ado를 예로 들면, ado는 기본적으로 one-node가 중앙상태를 atomic하게 바꾸면(타 함수의 작동에 영향을 미치는 시점) 되지만, paxos는 타 node로의 deliver 여부가 상태를 결정한다(타 함수의 작동에 영향을 미치는 시점). ADO state와 paxos state의 refinement 관계를 설정해도, 실제 target의 global state transition이 너무 느려 interaction point에서의 적절한 invariant를 설정해주기가 힘들다. 따라서 linearization point를 인위로 설정하여 허-공간과의 invariant를 설정한다. 그러나, 이 linearization point는 src의 global state를 결정하나, 결국 tgt가 실제 global state를 변화시킬때, 혹은 global state를 얻어올때, 이 global state가 src의 global state와 일치해야하므로(그래야 local transition이 일치하므로) 앞선 허-공간에서의 linearization point에서 tgt와 불일치하는 행위는 무시되어야한다(NB화, paritial termination이어도 된다). 따라서 이를 위해서 tgt와 불일치하는 부분을 잘라내면 tgt의 global state와 src의 global state가 서로 정상적인 invariant가 성립하여 동일한 local transition을 진행할 수 있다.
변화의 계기: 모델에서 spec으로의 사고 전환
ado는 꼭 필요한 정보만 들어있고, 꼭 필요한 정보만 유출 시킨다.
raft-ado method = append entry
paxos-ado method = write storage
11/1일 랩미팅 물어보기
triggerNB를 완전한 nb로 해석한다면, 이미 존재하는 simulation은 arbitrary nb를 증명할 수 없는 시점에서 이미 sound 하지만 complete하지 않다. 하지만, triggerNB를 partial termination으로 해석한다면, simulation은 complete하다.