확률론적, 리소스 인식, 비동기식, 순서 무시 코레오그래피

순서가 뒤바뀐(out-of-order) 코레오그래피의 Futures 기반 구현은 지연 시간과 처리량(throughput)을 크게 향상시킬 수 있지만, 실제 동작은 통신 지연(communication delay), 계산 시간(computation time), 실패, 그리고 복구와 같은 리소스에 따라 달라진다. Ozone의 O3와 같은 기존의 형식 모델들은 어떤 실행이 가능한지 설명하지만, 그러한 실행이 얼마나 가능성이 높은지 또는 얼마나 오래 걸리는지는 직접적으로 설명하지 못한다. 본 논문에서는 순서가 뒤바뀐 실행을 가진 비동기식 코레오그래피의 의미론(semantics)을 모델링하기 위한 확률론적이고 리소스 인식적인 언어인 AsInst를 제시한다. AsInst 프로그램은 런타임에 생성되는 값과 해당 값이 사용 가능해지는 시간을 모두 모델링하는 시간적 베이즈 네트워크(temporal Bayesian networks)로 해석된다. 우리는 이 핵심 의미론이 대응하는 futures 스타일의 네트워크 의미론을 정확하게 포착함을 증명한다. 또한, AsInst가 Ozone 스타일의 select-and-merge 조건문을 인코딩할 수 있음을 보여주고, 사례 연구를 사용하여 통신 실패 복구(communication-failure recovery)를 모델링하고 런타임 성능을 분석한다.