얼마 전까지만 해도 한글과컴퓨터 한글이나 마이크로소프트 워드를 사용하는 사람들은 ‘맞춤법 검사’ 실행을 구체적으로 지시해 철자 오류를 검사했다. 하지만 요즘은 철자 검사·수정은 사용자들이 글을 쓸 때 자동으로 실행된다.

이는 실시간으로 다른 프로그램과 동시에 실행되는 컴퓨팅 형태다. 현재 동시 프로그램은 운영체제(OS)에서 여러 응용 프로그램, 워드 프로세싱, 웹 브라우징에 이르기까지 사람들이 매일 사용한다.

카네기멜론대학 사이랩(CMU CyLab) 브라이언 파노(Bryan Parno) 컴퓨터과학부 교수 연구팀은 개발자가 프로그램 작성 시 코드 오류를 찾아 곧바로 수정하는 동시 프로그램을 위한 새로운 코딩 언어와 도구인 ‘아마다(Armada)’를 개발했다. 즉, 코드가 수학적으로 정확하게 계산됐는지 검사하고 수정하는 것이다.

연구 결과(논문명: Armada: Low-Effort Verification of High-Performance Concurrent Programs)는 최근 프로그래밍 언어 설계 및 구현에 관한 컨퍼런스 ‘PLDI 2020’에서 발표했으며 우수 논문상을 받았다.

<이미지를 클릭하시면 크게 보실 수 있습니다>

아마다(Armada)는 C 언어와 같은 작은 단계의 상태 머신 기반 시맨틱을 통해 개발자에게 임의 메모리 레이아웃과 동기화 프리미티브(기계 언어에서 가장 기본적인 명령어)를 선택할 수 있는 유연성을 제공하기 때문에 성능에 제약을 받지 않는다.

아마다는 개발자 노력을 줄이기 위해 기존에 입증된 기술을 사용한다. ‘SMT(통계 기반 기계번역, Statistical Machine Translation) 기반 자동화와 TSO(시분할 선택기능, Time Sharing Option) 소거(elimination), 축소(reduction), 별도 분석(alias analysis) 등 입증된 추론 기술 라이브러리를 활용한다.

연구팀은 “아마다는 매우 유연하게 설계돼 원하는 방식으로 코드를 작성할 수 있다. 정확하게 버그를 잡고 수정하며 백엔드(back end) 어떤 것도 망치지 않을 것”이라고 강조했다.

아마다는 급여 시스템에서 병원 기록, 모든 종류의 전자 상거래에 이르기까지 광범위한 응용 프로그램을 동시에 작성하는 모든 개발자에게 매우 유용할 것으로 기대된다.

김들풀 기자 itnews@