POPL 2011 & VMCAI 2011 January 23-28, 2011, Austin, TX, USA 서울대학교프로그래밍연구실, 조성근 두근거림 재작년 APLAS 09를서울에서했기때문에국제학회참가가이번이처음은아닙니다만이번에는그때와느낌이아주많이달랐습니다. 그때는갓입학하여학회가어떤것인지에대한감각이거의없었습니다. 친숙한학교에서했기때문에 외국인들이우리학교에서발표를하는구나. 정도로생각했습니다. 하지만이번에는달랐습니다. 학회에논문을제출하여발표하기까지얼마나많은노력이필요한지선배들의모습을통해짐작할수있었고, 그곳에모이는석학들이얼마나유명한지도알고있었기때문입니다. 저는두근거리는마음으로인천공항을출발하였습니다. 서울대학교프로그래밍연구실, 조성근 1
오스틴 오스틴의날씨는서울보다훨씬따뜻했습니다. 밤에도반팔차림으로밖을돌아다니는미국인을쉽게찾아볼수있었습니다. 음식은치즈가다소많기는했지만대부분입에맞았습니다. 오스틴에있는텍사스대학을구경하였습니다. 땅이넓어서인지모든건물이널찍널찍하게들어서있었고학생들은대부분당차게걷고있었습니다. 텍사스의여유롭고활기찬분위기를동시에느낄수있었습니다. 만남 학회참가는다른연구자들을만나는아주좋은기회가되었습니다. Lucas Brutschy는작년에 6개월간 ROPAS에서함께생활했었고, 오학주학생과함께연구하여 VMCAI에논문을합격시켰습니다. 함께생활하던 Lucas를만나굉장히반가웠고많은이야기를나누었습니다. 최원태학생과함께연구했던 Makoto Tatsuta 교수님, Baris Aktemur 교수님도만나서현재제가하고자하는연구에대해이야기하고많은조언을얻을수있었습니다. 양홍석교수님과허충길박사님도만나뵈어학회에임하는자세에대한좋은이야기도들을수있었습니다. 예상했던대로인터넷으로만보아오던연구자들을직접볼수있었습니다. 요약해석을만드신 Cousot 교수님부부가바로옆에서빵을드시고계셨는데마치제가동화속에들어온기분이었습니다. Coq을공부하면서알게된 Xavier Leroy, Adam Chlipala, David Pichardie도눈에띄었습니다. 쉬는시간에 Adam Chlipala가계단옆에쪼그려앉아컴퓨터를하고있는모습을보았습니다. 잠시후에보았더니그짧은쉬는시간동안 Coq 메일링리스트에답변을달았던서울대학교프로그래밍연구실, 조성근 2
것이었습니다. 언제어디서든지자신의일에열정을쏟는모습이인상적이었습니다. David Pichardie에게는 Coq을이용한분석기의안전성검증에대한질문을하였습니다. 날카로운인상에약간은무서웠지만차근차근친절하게설명해주었고이메일로관련자료도보내주었습니다. 느낀점 예전에이원찬학생이 trip report에서지적한부분들을몸소체험할수있었습니다. 1. 프로그래밍언어연구의다른분야도알자. 2. 내연구에대한소개를준비하자. 3. 영어로대화가잘될수있도록하자. 다른사람과대화를하려면내연구가있어야하고이를잘소개할수있어야합니다. 만약아직결과가나온연구성과가없는경우에는소개할것이없어난감합니다. 이럴때에는상대방의연구를이해하고궁금한점을물어볼수있어야합니다. 막상가서보니발표되는논문의분야가생각보다훨씬많음을느꼈습니다. 각분야에대한기초지식을알고있었다면더욱많은것을이해하고궁금해할수있었으리라생각합니다. POPL 11 과 VMCAI 11 의논문제목중여러번등장하는단어를모아보았습니다. Automata 나 Concurrency 와같이저에게는친숙하지않은단어가상당히크게자리잡 고있었습니다. 서울대학교프로그래밍연구실, 조성근 3
VMCAI Practical Verification for the Working Programmer with CodeContracts and Abstract Interpretation (Invited Talk) - Francesco Logozzo VMCAI'11 의첫발표는 Francesco Logozzo 의튜토리얼이었습니다. 그는 precondition 과 postcondition 을명세하고검사하는방법인 CodeContract 을소개하고 그를위한분석기인 Clousot 을시연하였습니다. 이분석의특징은다음과같습니다. 1. 정적분석에기반하고있기때문에조건명세를제외한모든분석이자동으로 이루어지며종료가보장됨 2. FunArray 라는요약도메인을사용함으로써분석비용과분석정밀도사이에서명 세된조건을만족시키기위한적절한균형을찾아냄 3..NET 프레임워크의바이너리코드를직접분석하기때문에그위에서구현된모 든언어에대해서분석이가능함 발표에서중점적으로설명한부분은 FunArray 라는요약도메인이었습니다. 이요약 도메인은배열의값을효율적으로표현하면서정밀도를잃지않도록하는도메인입니다. 사용자가약간의 precondition, postcondition 만입력해주면언어의의미를이용하여분 석을자동으로, 정밀하고, 빠르게해준다는점에서큰의미가있는연구인것같습니 다..NET 프레임워크위에서프로그래밍을할기회가생긴다면한번사용해보고싶다 는생각이들었습니다. Access Analysis-Based Tight Localization of Abstract Memories - Hakjoo Oh, Lucas Brutschy, and Kwangkeun Yi 첫날에는 ROPAS 오학주학생의발표가있었습니다. 정적분석기에지역화 (localization) 기술을적용하는것 입니다. 이연구에서는 1) 전분석 (pre-analysis) 을통하여 분석할때에실제로접근하는메모리를안전하게어림잡 아이용하고 2) 지역화를적용시킬적절한코드블록을선 택하는알고리즘을제안하였습니다. 이두방법으로 90% 이상의분석속도향상을이끌어낼수있었습니다. 국내 에서의연구가세계최고의권위자들에게소개되고인정 받는다는것에큰감동을받았습니다. Access Nets: Modeling Access to Physical Spaces: Robert Frohardt - Bor-Yuh Evan Chang and Sriram Sankaranarayanan 물리적공간의접근제어정책을모델검사를이용하여검증하는연구입니다. ACCESS NETS 라고하는 formal modeling framework 를이용하여접근허가, 물리적 서울대학교프로그래밍연구실, 조성근 4
공간, 시간제약등을기술하게됩니다. 도달가능성 (reachability) 분석을통하여보안정책을검증함으로써모델검사기술이물리적접근제어정책검사에효과적임을보이고있습니다. 모델검사가프로그램이나회로가아닌다른분야에적용된경우를쉽게볼수없었기때문에흥미로운연구라고생각했습니다. 모델검사의응용에대한새로운시각을전달했다는점에서재미있는연구였고, 요약해석기술도프로그램의실행을미리어림잡는곳이아닌다른곳에서유용하게사용될수있지않을까하는생각을하게되었습니다. Static Analysis of Finite Precision Computations - Eric Goubault and Sylvie Putot 이연구에서는유한한정밀도의수를다루는프로그램이가지는잠재적인정밀도손실에대한분석을이야기하였습니다. 이러한분석에서얻고자하는것은프로그래머가의도한대로프로그램이동작하는가, 즉, 유한한정밀도의수를다룸으로써발생하는에러가어느정도되는지프로그램실행전에예측하는것입니다. 이번발표에서는부동소수점의정밀도분석에대한이론적인내용 (SAS 01) 과더불어 zonotopic이라는요약도메인을사용하여값들사이의관계정보를유지하며정밀도를분석하는방법에대해서설명하였습니다. 또한부동소수점분석기 Fluctuat를시연하였습니다. 미리분석기실행동영상을촬영하여발표함으로써발표시간을적절히조절한점, 실행도중중요한부분을빨간원으로미리표시한점이인상적이었습니다. 이론적인연구가실제분석기로구현됨으로써청중들에게더욱강한인상을남길수있었습니다. 이론과실재가공존하는것이얼마나중요한것인가를다시한번느낄수있었습니다. String analysis as an Abstract interpretation - Se-won Kim and Kwang-Moo Choe 요약해석에기반하여문자열을분석하는기술에관한내용입니다. 이연구에서요약된문자열은 reference pushdown automaton의 configuration 변화를기술하는술어 (predicate) 들로표현됩니다. 또한 bounded pushdown automata를이용하면모든 context-free 언어들을표현할수있고분석에필요한계산가능한 operator들을정의할수있습니다. 또한완전하지않은프로그램문자열에대한분석이가능합니다. 이는프로그램의개발도중에오류를찾아줄수있음을의미합니다. 현재카이스트에서이연구에의한구현이이루어지고있다고합니다. 이처럼이론적인연구에서시작하여실용적인분석툴이만들어지는것은매우바람직한연구의흐름이아닐까하고생각하였습니다. POPL POPL은 VMCAI와사뭇분위기가달랐습니다. VMCAI의배가넘은사람들이학회에참가한듯보였습니다. 쉬는시간에는학회장앞에서커피를마시며이야기를하는데발디딜틈이없을만큼꽉차있었습니다. 발표이외의프로그램도훌륭했습니다. 학회의서울대학교프로그래밍연구실, 조성근 5
장인 Thomas Ball 을비롯한여러연구자들이음악을연주하는시간도있었습니다. 맥주 를마시며, 음악을듣고, Xbox 게임을하고, 사람들과이야기하고. 매우즐거운시간이었 습니다. Verified Squared: Does Critical Software Deserve Verified Tools? (Invited Talk) - Xavier Leroy 개인적으로상당히기대하고있었던발표였습니다. 프로그램검증분야에서두드러진 업적을보이고있는 Xavier Leroy 의발표이기도하였고, POPL'11 의첫발표이기도하였 기때문입니다. 발표내용중가장인상적이었던부분은 Coq 으로안전성이검증된 C 컴파일러에관한 내용이었습니다. 이미알고있던내용이기는하였지만컴파일러의성능이이렇게좋을 것이라고는생각하지못했습니다. Compcert 라는컴파일러는 gcc 의최적화옵션을주는 것에비하여크게떨어지지않는성능을보였고일부프로그램에대해서는더나은성능 을보이기도했습니다. Coq 으로검증된프로그램이이렇게실용적일수있다는것에놀 라며실용적이고안전한프로그램을 Coq 으로만들어보고싶다고생각했습니다. <Xavier Leroy 의 LCTES 08 Invited Talk 슬라이드로부터 > 매끄러운발표진행과적절한도표사용이또한인상적이었습니다. 중요도순으로나열된프로그램, 프로그램의안전성을위한여러기술들과프로그램의관계, 컴파일러의동작순서와검증된부분에대한도표등은이분야에서진행되고있는연구들의큰그림을이해하는데에도움이되었습니다. 서울대학교프로그래밍연구실, 조성근 6
Static Analysis of Multi-Staged Programs Via Unstaging Translation - Wontae Choi, Baris Aktemur, Kwangkeun Yi, and Makoto Tatsuta ROPAS 의최원태학생의발표가있었습니다. 내용은이 전에 ROSAEC 워크숍에서발표한내용과같습니다. 이논 문에서는멀티스테이지언어로부터단계가없는언어로의 변환을정의하고변환이실행의미를보존함을증명하였습니 다. 또한변환결과물을이용하여원본프로그램을검증할 수있다는사실을증명하였습니다. 발표는성공적이었습니 다. 주어진시간을잘활용하여준비한내용을모두발표하 였습니다. Patrick Cousot 교수님께서밝게웃으며코멘트 를하려고뛰어나오셨습니다. 세계최고의석학들에게자 신의연구를소개하고코멘트와질문을받는일, 열심히훌 륭한연구를한연구자에게주어지는선물이라는생각이들 었습니다. Automating String Processing in Spreadsheets using Input- Output Examples - Sumit Gulwani Spreadsheet 에서편리하게쓰이는문자열변환에관한연구입니다. Sumit Gulwani 는 문자열의입력과출력의예를바탕으로변환함수를자동으로만들어내기위한언어와 알고리즘을제안하였습니다. 또한해당알고리즘을 Microsoft Excel 에장착하였고, 발표 시간의상당부분을프로그램시연에사용하였습니다. 덕분에이연구가정말유용하고 유용하며훌륭한연구라는생각이들었고논문을한번자세히읽어보고싶어졌습니다. 학회에서의발표는논문의내용을그대로읊는것이아니라발표자의논문을읽고싶어 하도록유도하는것이라하는데, 그러한점에서정말훌륭한발표였다고생각합니다. Spreadsheet 는다양한직종의사람들에의해서사용되는데그들모두가프로그래밍에 능한것이아니기때문에이연구가더욱유용하다고할수있습니다. 서울대학교프로그래밍연구실, 조성근 7
마치며 POPL 11 피드백조사에서 환태평양지역에서 POPL이열리면참가하시겠습니까? 라는질문이있었습니다. 확인해보니지금까지 POPL의 84% 가미국에서열렸고나머지 16% 가유럽에서열렸습니다. 지극히미국과유럽중심의학회가아시아의연구에귀를기울일준비를하고있다는점에서한국에서연구를하고있는우리에게는희망적인이야기가아닐까생각합니다. 감사합니다 세계최고수준의예술을만들고자하는예술가에게세계최고수준의예술작품을보여주는것만한선물은없을것이고, 세계최고수준의기업가가되고자하는사람에게세계최고수준의기업가와만날수있는기회를주는것만한선물은없을것입니다. 이번학회참가는석사 2년차꼬마인저에게그런느낌으로다가왔습니다. 세계최고수준의연구를직접보고느낄수있는기회. 덕분에많은것을생각하고배울수있었습니다. 제가이러한선물을받을수있도록도움을주신 ROSAEC 센터에깊은감사의뜻을전하고싶습니다. 이에보답하는길은훌륭한연구를열심히, 즐겁게하는것이겠지요. 서울대학교프로그래밍연구실, 조성근 8