PLDI'16 Trip Report Trip Report: Santa Barbara, CA, USA 2016/6/13 17 서울대학교 프로그래밍 연구실 조성근,, 출발 명실공히 프로그래밍 언어 분야 최고 학회인 에 다녀왔다 나는 에 처음으로 참여

Size: px

Start display at page:

Download "PLDI'16 Trip Report Trip Report: Santa Barbara, CA, USA 2016/6/13 17 서울대학교 프로그래밍 연구실 조성근,, 출발 명실공히 프로그래밍 언어 분야 최고 학회인 에 다녀왔다 나는 에 처음으로 참여"

신애 간
5 years ago
Views:

주로 시스템 검증과 합성 타입 시스템 관련된 발표를 들었다 다만 이상하게도 올해 에는 분석 관련 발표가 조금 적었다 각 세션 별 발표된 논문 수는 아래와 같다 (ACM Design

1 Trip Report: Santa Barbara CA USA 2016/6/1 17 서울대학교 프로그래밍 연구실 조성근 출발 명실공히 프로그래밍 언어 분야 최고 학회인 에 다녀왔다 나는 에 처음으로 참여하는 것이었기 때문에 훌륭한 연구 결과들을 구경할 생각에 출발 전부터 상당히 큰 기대를 가지고 있었다 총 편의 논문이 종류의 세션으로 나뉘어 발표되었고 나는 주로 시스템 검증과 합성 타입 시스템 관련된 발표를 들었다 다만 이상하게도 올해 에는 분석 관련 발표가 조금 적었다 각 세션 별 발표된 논문 수는 아래와 같다 (ACM Design and Implementation) conference on Programming Language 1/12

2 세션 논문 수 Down to the Metal 6 Types 6 Synthesis 5 Parallelism 5 Veri 5 ﬁ cation Energy & Performance New Languages Parsing & Compilation Security ﬁ Software De ned Networking Testing & Debugging Verifying System Memory Managemen 2 총 50 나리타에서 샌프란시스코 갈 때 탔던 비행기와 샌프란시스코에서 산타바바라 갈 때 탔던 비행기 멋지다! 생활 학회는 캘리포니아 산타바바라에서 열렸다 샌프란시스코에서 비행기를 갈아 타고 한 시간 남짓 더 날아가면 도착할 수 있는 곳이었는데 놀라울 정도로 산타바바라 공항의 크기가 작았다 비행기를 탈 수 있는 게이트가 고작 개 뿐이었다 아마도 국내선 밖에 없어서 그럴 것이었다 지금껏 국제선이 있는 인천공항 제주공항 만 을 봐 와서 인지 작은 공항이 상당히 인상적이었다 5 2/12

특이했는데 일단 생각보다 엄청 추웠다 왠지 해안가가 유명한 산타바바라는 날씨가 서울보다 더 울 것 같아서 긴팔 긴바지 옷 한 벌에 반팔 반바지 옷만 잔뜩 가져갔는데 바람이 너무 차가워서 긴팔 긴바지 옷 한 벌을 거의 일 주일 내내 입은 것 같다 사람들에게 물어보니

3 음식 학회가 열린 산타바바라는 와인과 맥주가 유명하다고 했는데 아쉽게도 와인은 먹을 기회가 없었다 맥주도 특 별한 가게를 찾아 간 것은 아니지만 같은 지역 고유의 맛있는 맥주를 몇 번 마실 기회 가 있었다 학회에서는 아침마다 빵을 주었고 점심엔 뷔페를 주어서 우리들이 특별히 음식을 사 먹을 필요가 없었다 다 만 학회장 근처에 음식점이 너무 없어서 음식을 제공 받지 않았으면 점심을 먹기가 매우 까다로웠을 것 같았 다 805 Hoppy Poppy IPA 학회장 근처에 유일하게 있던 햄버거 가게 Habit 날씨 날씨는 조금 특이했는데 일단 생각보다 엄청 추웠다 왠지 해안가가 유명한 산타바바라는 날씨가 서울보다 더 울 것 같아서 긴팔 긴바지 옷 한 벌에 반팔 반바지 옷만 잔뜩 가져갔는데 바람이 너무 차가워서 긴팔 긴바지 옷 한 벌을 거의 일 주일 내내 입은 것 같다 사람들에게 물어보니 산타바바라는 일 년 내내 기온이 비슷하다고 하 던데 정말 그럴 수도 있을 것 같다 위키피디아에 따르면 서울은 북경 이고 산타바바라는 북경 인데 어 떻게 이럴 수가 있는지 신기하다 /12

학회장 근처의 해변 거리 거리는 진짜 미국답게 넓었다 층이 넘는 건물도 거의 찾아볼 수 없었고 모든 주차장은 지상에 있었다 오 후에는 해변가이다 보니 사람들은 아름다운 석양을 맞으며 조깅을 하고 있었고 동네에 있는 운동장마다 사람 들이 옹기종기 모여 축구나 야구를 하고 있었다 잔디밭이 여기저기 넓게 펼쳐져 있었는데 내 몸집만한 개들 이 공을 물어오며

4 학회장 근처의 해변 거리 거리는 진짜 미국답게 넓었다 층이 넘는 건물도 거의 찾아볼 수 없었고 모든 주차장은 지상에 있었다 오 후에는 해변가이다 보니 사람들은 아름다운 석양을 맞으며 조깅을 하고 있었고 동네에 있는 운동장마다 사람 들이 옹기종기 모여 축구나 야구를 하고 있었다 잔디밭이 여기저기 넓게 펼쳐져 있었는데 내 몸집만한 개들 이 공을 물어오며 즐거운 시간을 보내고 있었다 특이한 것은 길거리에 키가 매우 큰 야자수들이 있었는데 그 광경이 너무 생소해서 비현실적으로 느껴지기까 (?) 2 지 했다 공기가 맑아서 시야가 매우매우 멀다 관광 호텔에서 지나가던 사람이 산타바바라에 잘 왔다며 스테이트 스트리트에 꼭 가 보라고 했다 그곳에 가면 사 람도 많고 쇼핑몰도 많고 맛있는 음식점도 많다고 했다 학회가 끝나고 시간이 남아 종권이와 함께 구경을 떠 났다 그 사람 말대로 스테이트 스트리트엔 옷을 파는 쇼핑몰과 음식점이 많았는데 우리가 딱히 옷을 사고 싶 은 것은 아니어서 맛있는 피자와 맛있는 스파게티 스테이크를 먹고 집으로 돌아왔다 4/12

5 스테이스 스트리트에 있던 스타벅스 커피 연구 이야기 포스터 발표 에 참여하여 포스터를 발표하였다 우수한 포스터로 선발되면 의 세션에서 분 간 연구를 발표할 수 있는 기회를 얻게 되고 거기에서 또 우수한 발표로 선발되면 상금과 함께 에 초대 받는다고 한다 우리 연구실에서는 세 편의 포스터를 발 표하였지만 안타깝게도 본선에 진출하지는 못했다 SRC(Student Research Competition) SRC 15 Annual ACM Awards Banquet 5/12

SRC 포스터 발표장 ZooBerry: Automatic Generation of Sparse Global Static Analyzers & Their Validators

없는 포스터였기 때문에 이 야기하고 싶은 내용을 간단히 표현하는 것이 목표였다 연구 배경 스파스 분석 기술 덕분에 정적 분석기의 성능에 비약적인 발전이 있었다 문제 스파스 분석 기술

로부터 개의 버그를 찾았는데 그 중 개가 스파스 분석 기술 적용 에 관한 것이었다 또한 일반적으로 분석 결과 요약 상태 는 눈으로 볼 수 없을 만큼 크기 때문에 테스팅으로 분석기의

6 SRC 포스터 발표장 ZooBerry: Automatic Generation of Sparse Global Static Analyzers & Their Validators Sungkeun Cho and Kwangkeun Yi 내가 발표한 연구는 최적화된 분석기와 검산기의 자동 생 성에 대한 것이었다 지난 에서 발표했던 내용과 거 의 비슷했으나 애니메이션이 없는 포스터였기 때문에 이 야기하고 싶은 내용을 간단히 표현하는 것이 목표였다 연구 배경 스파스 분석 기술 덕분에 정적 분석기의 성능에 비약적인 발전이 있었다 문제 스파스 분석 기술 적용은 번거롭다 데이터 의존 그래프를 그리기 위한 전분석을 구현해야 하는 데 기존의 에서는 이것이 약 줄을 차지했다 문제 스파스 분석 기술 적용은 틀리기 쉽다 우리 는 지난 연구에서 로부터 개의 버그를 찾았는데 그 중 개가 스파스 분석 기술 적용 에 관한 것이었다 또한 일반적으로 분석 결과 요약 상태 는 눈으로 볼 수 없을 만큼 크기 때문에 테스팅으로 분석기의 버그를 찾는 것은 쉽지 않다 SIGPL : 1: SparseSparrow : SparseSparrow 1 5 ) ( 6/12

7 해결 위의 두 문제를 해결하기 위해 우리는 자동 분석기 검산기 생성 시스템 을 제안한다 사용자가 분석 명세를 건내면 는 스파스 분석이 적용된 분석기와 분석 결과를 검산하는 검증 된 검산기를 생성한다 몇몇 연구자들이 와서 포스터 발표를 들었지만 분석에 집중된 학회가 아니어서 인지 특별히 인상적인 코멘트 는 없었다 아쉬웠다 그래도 스파스 분석을 이미 알고 있는 한 연구자가 전분석의 디자인에 대해 구체적인 내 용을 물어봐서 내가 알고 있는 내용을 이야기할 수 있었다 그 사람이 흥미롭다며 연구가 혹시 연구 내용이 출 판되었냐고 물어봤고 아직 아니라고 하자 포스터의 사진을 찍어 갔다 비록 많은 사람들이 포스터를 보러 온 것은 아니었지만 내가 만든 무언가를 누군가가 의욕적으로 소비했다는 것에 기분이 좋아졌다 : / (ZooBerry) ZooBerry 논문 발표 이번 는 대략 개의 위성 학회 워크숍과 함께 했다 나처럼 하여 대략 그 내용을 살펴 보면 다음과 같다 7 / 를 처음 가거나 가보지 못한 사람들을 위 ARRAY(ACM SIGPLAN International Workshop on Libraries Languages and Compilers for Programming) 이름을 보고 설마했는데 정말 배열 구조에 관련된 워크숍이라고 한다 주로 수치 계산을 빠르고 간결하 게 하는 방식에 대한 내용을 다룬다고 한다 FMS(Workshop on Formal Methods and Security) 보안 문제를 해결하는 데에 정형 기법 이나 프로그래밍 언어의 기술을 적용하는 방법 을 다룬다 구글의 로부터 정적 분석 기술을 사용하여 안드로이드 앱들의 악성 행 동을 잡는 초대 발표가 있었던 워크숍이었다 (formal method) Gogul Balakrishnan ISMM(ACM SIGPLAN International Symposium on Memory Management) 메모리 관리에 관련된 주제를 다룬다 메모리 재활용이나 효율적인 데이터 구조 메모리 구조 등 생각보 다 프로그래밍 언어 분야의 많은 주제들이 메모리와 관련되어 있다 LCTES(ACM SIGPLAN/SIGBED Conference on Languages Compilers Tools and Theory for Embedded Systems) 이름대로 임베디드 시스템과 관련된 프로그래밍 언어 컴파일러 이론 등을 다루는 학회이다 논문이 개나 발표되는 작지 않은 학회였다 20 PLMW(ACM SIGPLAN Programming Languages Mentoring Workshop) 학부생이나 석사과정 학생 박사과정 학생 초년생들에게 프로그래밍 언어 분야의 연구를 소개하는 워 크숍이다 프로그래밍 언어 분야 최근 연구 동향 등의 기술적인 내용 뿐 아니라 연구를 잘 하기 위해 필 요한 덕목에 대해 이야기하기도 한다 SOAP(ACM SIGPLAN International Workshop on the State Of the Art in Java Program Analysis) Java 분석을 위한 최신 기술을 다루는 워크숍이다 분석에 관련된 재미난 초대 발표들이 있었다 X10(ACM SIGPLAN Workshop on X10) 이라는 병렬 프로그래밍을 위한 언어에 대한 워크숍이다 은 를 뜻한다고 한다 이렇게 많은 종류의 학회 워크숍이 있었지만 동시다발적으로 발표가 열리는 바람에 극히 일부만을 듣고 소화 할 수 밖에 없어서 안타까웠다 예를 들어 도 두 세션이 항상 함께 열렸는데 시스템 검증과 타입 시스템이 계속 같이 열리는 바람에 타입 관련 발표는 절반 밖에 듣지 못했다 예전에 처음 이런 시스템을 접했을 때엔 내 가 듣고 싶은 것을 선택한다는 것이 매력적이라고 생각했는데 이번에는 선택을 해야만 하는 것이 안타깝게 느 X10 "X10" boost" "ten times productivity / 7/12

8 껴졌다 장단이 있는 것 같다 일 간 여러 발표를 들었는데 인상적이고 기억에 남는 발표를 정리하면 아래와 같다 5 [Tutorial] Programming using Examples Sumit Gulwani and Oleksandr Polozov 가 연구해 온 프로그래밍 합성에 대한 이야기였다 지금껏 연구된 다양한 프로그래밍 합성을 보이고 그 원리를 소개했다 특히 프로그래밍을 잘 못하는 혹은 하기 귀찮은 사람들을 위해서 입출력 예를 통 Sumit Gulwani 해 합성을 수행하는 방법을 주로 이야기했다 가 해 온 성공적인 프로그램 합성의 중요한 줄기 중 하나가 도메인에 특화된 언어 ﬁ 의 정교한 디자인이다 프로그램 합성이 어려운 이유 중 하나는 일반적인 프로그래밍 언 어의 경우 프로그램의 공간이 매우 넓다는 것이다 즉 개념적으로 프로그램 합성이란 것은 전체 프로그램 공 간에서 어떤 성질을 만족하는 프로그램을 찾는 과정인데 전체 프로그램 공간이 너무 크면 합성이 어렵다는 것 이다 이러한 문제를 해결하기 위해 는 합성된 프로그램이 다루는 도메인에 따라 특화된 언어 를 디자인했다 예를 들어 을 다루는 프로그램을 합성할 때 스프레드시트의 값을 다루는 프로그램을 합 성할 때 로그 텍스트 파일을 다루는 프로그램을 합성할 때 각각에 적합한 언어를 디자인했다 또한 이런 특화 된 언어를 디자인할 때에는 역함수 등이 존재하는지 효율적으로 구현 가능한지 등등이 합성의 성능에 영향을 주는 요인이라고 설명했다 프로그램 합성의 또 다른 중요한 줄기는 입출력 조건을 만족하는 여러 함수가 발견되었을 때 그 중 더 나은 함 수를 고르는 방법에 대한 것이었다 여러 가지 방법이 있을 수 있는데 직관적으로 가장 맞을 것 같은 느낌이 드 는 것은 작은 크기의 프로그램을 더 나은 함수로 고르는 것이다 물론 어떤 프로그램이 더 작은 프로그램인지 를 결정하는 것 또한 애매한 일이다 발표에서는 이러한 애매함을 보여주는 여러 가지 예들을 소개했고 더 올 바른 함수를 고르기 위해 머신러닝을 적용하기도 한다고 했다 다양한 그리고 아주 구체적인 적용 성공 사례가 있는 것은 좋지만 각 문제마다 너무 특별한 방법이 사용되는 것은 아닌가 하는 생각했다 새로운 도메인이 나타났을 때 이에 특화된 언어를 디자인하는 것은 그것 다루는 라이브러리 함수 모음을 구성하는 것과 비슷한 동작이 아닐까 생각했었는데 이때 합성의 성능까지 고려해야 한다니 디자인이 쉬워 보이진 않는다 (domain Sumit Gulwani speci c language) Sumit Gulwani XML / 만찬이 있었던 산타바바라 해양 박물관 앞 8/12

9 [SOAP] Toward an Automated Benchmark Management System Lisa Nguyen Quang Do Michael Eichberg and Eric Bodden 프로그램 분석의 평가를 위해서 벤치마크를 자동으로 구성하는 방법에 대한 연구였다 먼저 벤치마크가 만족 했으면 하는 성질에 대해서 이야기했는데 다음의 세 가지였다 장난감 코드가 아닌 실제 세계의 코드 최근까지 유지 보수되는 코드 컴파일 가능한 코드 저자들은 로부터 위의 세 조건을 만족하는 코드를 반자동으로 모으는 시스템을 소개하였다 먼 저 위 세 조건 중 는 코드의 크기를 확인한다던가 가장 최근의 커밋 날짜를 확인함으로써 기계적으로 가능 하다 하지만 아직 컴파일을 자동으로 하기는 쉽지 않았다고 한다 많은 프로젝트들이 유사한 빌드 프로세스 를 가지고 있기도 하지만 일반적으로 프로젝트의 규모가 커질 수록 빌드 프로세스가 점점 복잡해지기 때문이 의 패키지와 같이 시스템 종류에 상관없이 자동으로 빌드될 수 있는 시스템을 이용하는 다 코멘트 중 것이 어떻겠냐는 이야기가 있었는데 정말 괜찮은 아이디어라고 생각했다 엄청나게 새로운 내용이거나 반짝이는 아이디어가 숨어 있었던 것은 아니지만 벤치마크를 필요로 하는 우리 에게 좋은 영감을 주는 연구가 아니었나 생각한다 1 2 / GitHub Java 1 2 Docker [ISMM] Liveness Based Garbage Collection for Lazy Languages Prasanna Kumar Amitabha Sanyal and Amey Karkare 메모리 재활용 을 메모리 도달 가능성 에 기반하여 하는 것이 아니라 추 후 메모리 사용 가능성 에 기반하여 수행하는 방법에 대한 연구이다 즉 앞으로 실행할 프로그램을 분석하여 사용할 가능성이 조금이라도 있는 메모리를 남기고 나머지를 재활용하는 방식이다 이 방법을 사용 하면 기존 방법에 비해서 프로그램의 최대 메모리 사용량을 줄일 수 있으면서도 메모리 재활용에 필요한 시간 은 비슷하다고 한다 언뜻 생각하면 더 비싼 분석을 수행하기 때문에 메모리 재활용에 항상 더 많은 시간이 필 요할 것으로 생각되지만 더 적은 메모리를 관리함으로써 얻는 시간적인 이득이 있는 것으로 보인다 적극적으로 계산하는 언어 에 대해서는 같은 메모리 재활용 방법을 사용하는 기존의 연구 를 대상으로 한다 소극적으로 계산하는 언어 가 있지만 이 연구는 소극적으로 계산하는 언어 에서는 덜 계산된 식이 힙 메모리에 기록될 수 있기 때문에 추후 메모리 사용 가능성을 분석하는 기존의 간단 하면서 효율적인 방법이 바로 적용되기는 어렵다고 했다 이 문제를 해결하기 위해 저자들이 제안한 분석 방 법의 핵심은 다음과 같다 덜 계산된 식을 마저 계산할 때 필요한 변수들을 구하고 덜 계산된 식이 만들어지는 위치부터 실제 계산이 될 수 있는 위치까지 계산에 필요한 변수들이 사용될 수 있다고 안전하게 분석함 아직까지 이 문제에 대한 해결법이 나오지 않았다는 것이 이상할 정도로 간단한 해결 방법이라고 생각했다 (garbage collection) (reachability) (liveness) (eager language) (lazy language) /12

학회장에서 약간 떨어진 태국 음식점에서 내 생애 첫 파타이 [] Verifying Bit Manipulations of Floating Point Wonyeol Lee Rahul Sharma and Alex Aiken 미국에서 유학 중인 이원열 학생의 부동소수점을 다루는 함수들의 검증에 대한 연구 발표였다 일반적으로 컴 퓨터의 부동소수점 연산은 오차를

혼재되어 어셈블리로 적혀있을 뿐이다 이러한 공격적인 부동소수점 연산의 오차 범위를 추론하기 위해 이 연구에서는 입력으로 주어질 수를 여러 그 룹으로 나누어 각각의 최대 오차 범위를 계산하는 방법을 사용한다 여기서 그룹을 나누는 기준이 중요한데 같은 그룹에 속한 수들은 알고리즘에 존재하는 비트 연산이 같은 값으로 실행되도록 한다 즉 하나의 오차 범 위 추론

10 학회장에서 약간 떨어진 태국 음식점에서 내 생애 첫 파타이 [] Verifying Bit Manipulations of Floating Point Wonyeol Lee Rahul Sharma and Alex Aiken 미국에서 유학 중인 이원열 학생의 부동소수점을 다루는 함수들의 검증에 대한 연구 발표였다 일반적으로 컴 퓨터의 부동소수점 연산은 오차를 가지기 때문에 관련 검증의 내용은 가능한 부동소수점 오차 범위에 대한 경 우가 많다 이 연구에서는 비트를 직접 다루는 공격적인 부동소수점 연산의 검증을 다루고 있는데 기존의 연 구들에서는 다루지 못했던 것이라고 한다 이 문제의 어려움은 공격적인 알고리즘이 애초에 왜 올바른지에 대 한 직관을 가지기 어렵다는 것이다 단지 여러 비트 연산과 부동소수점 연산이 혼재되어 어셈블리로 적혀있을 뿐이다 이러한 공격적인 부동소수점 연산의 오차 범위를 추론하기 위해 이 연구에서는 입력으로 주어질 수를 여러 그 룹으로 나누어 각각의 최대 오차 범위를 계산하는 방법을 사용한다 여기서 그룹을 나누는 기준이 중요한데 같은 그룹에 속한 수들은 알고리즘에 존재하는 비트 연산이 같은 값으로 실행되도록 한다 즉 하나의 오차 범 위 추론 문제를 여러 추론 문제로 바꾸고 그 이후에 비트 연산을 추론이 쉬운 다른 것으로 변환하여 문제를 푸 는 것이다 어려운 내용을 쉽게 설명하는 발표가 인상적이었다 사실 부동소수점 문제가 워낙 복잡하기 때문에 논문에서 말하는 모든 디테일을 이해하기는 어렵다 하지만 발표에서는 나같은 수학 문외한도 무엇이 문제이고 대략 어 떻게 풀었는지 이해할 수 있도록 큰 그림을 위주로 설명했다 10/12

[] MapReduce Program Synthesis Calvin Smith and Aws Albarghouthi 스타일의 프로그램을 자동으로 생성하고자 한다 이 연구에서는 입출력 예들로부터 맵리듀스 다른 합성 연구와 비슷하게 도메인에 특화된 언어를 사용했으며 탐색할 프로그램의 공간을 줄이기 위해 프로 과 타입 시스템을 이용했다 프로그램 틀의 모양은

11 [] MapReduce Program Synthesis Calvin Smith and Aws Albarghouthi 스타일의 프로그램을 자동으로 생성하고자 한다 이 연구에서는 입출력 예들로부터 맵리듀스 다른 합성 연구와 비슷하게 도메인에 특화된 언어를 사용했으며 탐색할 프로그램의 공간을 줄이기 위해 프로 과 타입 시스템을 이용했다 프로그램 틀의 모양은 다음과 같다 그램 틀 (MapReduce) (template) mapf reduceg 개별 문제를 푸는데에 사용하는 함수 와 개별 결과를 하나로 모으는 함수 를 합성하는 것이다 여기까지는 다른 합성 연구와 크게 다르지 않지만 리듀스 함수 가 만족해야 하는 특별한 성질이 있다 위해서는 함수 가 합성된 맵리듀스 스타일 프로그램이 항상 같은 입력에 같은 출력을 내기 다음 두 조건을 만족해야 한다 이 연구에서는 합성된 가 위의 조건을 만족하는지 자동으로 검사하는 분석을 제시했다 동적 분석 입출력 예들을 이용해서 가 위의 조건을 만족하는지 확인 정적 분석 동적 분석에 성공햇다면 를 이용하여 가 위의 조건을 만족시킴을 확인 f g g (deterministic) g x y z : g(g(xy)z) = g(xg(yz)) associative: commutative: x y : g(xy) = g(yx) g 1 : g 2 : SMT solver g 풀고자 하는 문제도 명확했고 방법도 직관적이서 듣기 좋았던 발표였다 특히 예제를 통해서 맵리듀스 스타일 의 프로그램이 합성되는 과정을 차근차근 설명한 부분이 좋았다 유나이티드 항공 비행기에서는 좌석마다 을 제공한다 비행기 내에서 각자의 노트북을 이용하라는 뜻 Private Screen(?) ﬁ [] Veri ed Peephole Optimizations for CompCert Eric Mullen Daryl Zuniga Zachary Tatlock and Dan Grossman 백앤드의 꼬마 최적화들 을 검증하는 연구다 우리 연구 그룹도 의 꼬마 최적화들 을 검산하는 연구를 했었기에 그것과 비슷하지 않을까 생각했는데 꼭 그렇지는 않았다 우리는 주로 많은 수의 꼬마 최적화들을 적은 비용으로 검산하는 데에 초점이 있었는데 이 CompCert (peephole optimization) LLVM (instcombine pass) 11/12

연구는 주로 다음과 같은 주제들에 초점이 있었다 어셈블리 메모리 모델 확장 이 연구의 대상은 백앤드에서의 꼬마 최적화 들이다 그 최적화들 중 어떤 것들은 메모리 주소가 실제 정수 이어야 하는데 의 그것은 논리적인 주소 라는 것이다 그래서 저자들은 어셈블리가 실제 정수 메모리 주소를 사용하도록 확장했다고 한다 이러한 확장은 강지훈 학생과 허충길

깨달았고 개인적으로 이것이 연구에 박차를 가하는 데에 도움이 될 것 같다 CompCert x86 : CompCert (physical CompCert x86 (logical address) address) x86 CompCert A Formal C Memory Model Supporting Integer Pointer Casts CompCert

12 연구는 주로 다음과 같은 주제들에 초점이 있었다 어셈블리 메모리 모델 확장 이 연구의 대상은 백앤드에서의 꼬마 최적화 들이다 그 최적화들 중 어떤 것들은 메모리 주소가 실제 정수 이어야 하는데 의 그것은 논리적인 주소 라는 것이다 그래서 저자들은 어셈블리가 실제 정수 메모리 주소를 사용하도록 확장했다고 한다 이러한 확장은 강지훈 학생과 허충길 교수님께서 참여한 작년 연구 보다 덜 강력한 확장이지만 대상으로 하는 최적화가 간단 한 것들이어서 이것만으로도 충분했던 것이라 생각했다 에서의 추후 메모리 사용 가능성 분석 특정 위치에서의 최적화가 추후의 실 행에 영향을 주지 않음을 보장하기 위해 변경된 값의 사용 여부를 분석한다 세상에 많은 사람들이 비슷한 문제로 고민한다는 것을 다시 한 번 깨달았고 개인적으로 이것이 연구에 박차를 가하는 데에 도움이 될 것 같다 CompCert x86 : CompCert (physical CompCert x86 (logical address) address) x86 CompCert A Formal C Memory Model Supporting Integer Pointer Casts CompCert x86 (liveness) : 마치며 언제나 학생들에게 좋은 기회와 지원을 주시는 이광근 교수님 허충길 교수님 감사드립니다 또한 학회 방문 에 차질이 없도록 힘써 주신 최은희 선생님께도 감사드립니다 학회장 바로 옆 기찻길 기차가 지나갈 때마다 큰 경적 소리가 울린다 12/12

Microsoft PowerPoint - chap01-C언어개요.pptx

Microsoft PowerPoint - chap01-C언어개요.pptx #include int main(void) { int num; printf( Please enter an integer: "); scanf("%d", &num); if ( num < 0 ) printf("is negative.\n"); printf("num = %d\n", num); return 0; } 1 학습목표 프로그래밍의 기본 개념을