아마존 웹서비스와 TLA+ 방법

전문가 제언

○ 병렬 컴퓨팅은 메모리상에서 연산방법과 결과의 출력구성 규칙을 정의하는 일관성 모델을 필요로 한다. 레슬리 램포트의 순차 일관성(sequential consistency)모델은 병렬 프로그램 실행시 순차프로그램에서 나오는 결과와 동일하게 구성되는 프로그램 특성을 보유한다. 특히 실행결과가 모든 프로세서들의 순차적 연산 프로그램과 같다면 프로그램은 순차적으로 모순이 없다는 것으로 일관성을 지칭한다.

 

○ 일관성모델의 원조인 페트리 넷을 기반으로 자료흐름 이론이 생성되었고 통신 시스템이나 순차프로세스 미적분 구성요소들의 개발 이래 동적 기하학에 의한 성능 향상 프로세스가 추가되었다. 램포트의 TLA, 대각합(traces)이나 액터 이벤트 다이어그램 (Actor event diagrams) 같은 수학적 모델들이 시스템의 동기적 행위 메커니즘을 설명하기 위해서 생성되어 왔다.

 

○ 본고에서는 AWS 엔지니어들이 실사례와 경험에 입각하여 그들이 핵심적 통찰한 내용을 중심으로 그들의 의견을 피력하였다. 일견 TLA+의 선호로 보여질 수 있으나 엔지니어들의 통찰이란 측면에서 참조할 만한 점이 있다. 그들의 주장은 공식적인 방법만이 시스템 설계의 버그를 잡을 수 있고, 사용하기 쉬우며 양호한 투자수익률을 시현한다는 점이며, 아마존에서는 공공 클라우드 서비스를 포함하여 실제 소프트웨어 설계에 이 방법이 정기적으로 적용된다는 점을 언급한다. 요약하면 코드 시험의 부적절함에 기인하여 더 개선된 방법을 제시한다는 것이다.

 

○ 아마존 엔지니어들은 Dynamo DB 장애처리에 TLA+를 참조하고 PlusCal 일부와 TLA+를 정련해 가면서 이 방법에 대한 통찰력을 생성해오고 있다. 그들은 관계형 DB나 No-SQL 데이터베이스 스키마 설계시 TLA+가 데이터 모델링에 탁월함을 발견했다. 본고에서 공식적 방법의 장단점, 진화과정을 언급하며 TLA+ 우수성을 강조한다.

 

○ 그러나 공식적 방법도 시스템자체가 아니라 시스템 모델이므로 다 안 맞거나 몇 개만 유용할 수 있으므로 다자이너들이 모델이 유의미한 측면을 잡아내는지 반드시 확인해야 한다고 언급한다. 배울 점이 있다.

저자

CHRIS NEWCOMBE, TIM RATH, FAN ZHANG, BOGDAN MUNTEANU, MARC BROOKER, AND MICHAEL DEARDEUFF

자료유형

학술정보

원문언어

영어

기업산업분류

정보통신

연도

2015

권(호)

58(4)

잡지명

Communications of the acm

과학기술
표준분류

정보통신

페이지

66~73

분석자

박*만

분석물

• 아마존 웹서비스와 TLA+ 방법.pdf [367,258 byte]

이미지변환중입니다.