jssst sig-ppl

PPL 2015:招待講演

PPL2015では,2件の招待講演を予定しております.

橋本 和幸 NVIDIA. 元日本シンボリックス株式会社
1980年代のLispマシンSymbolicsとその開発環境Genera
付属:NVIDIA GPUによる超並列コンピューティング
Chung-Kil Hur Seoul National University
Formal C semantics and LLVM compiler validation

招待講演1: 1980年代のLispマシンSymbolicsとその開発環境Genera
      付属:NVIDIA GPUによる超並列コンピューティング

橋本和幸 (NVIDIA. 元日本シンボリックス株式会社)

橋本氏の写真

概要

Symbolics社は、1981年に設立されたLispマシンの専業メーカーで、既に倒産して現存していない。MIT AI Lab.で開発されたLM-2をベースに、独自の36ビットアーキテクチャを開発し商用Lispマシンとしての販売に成功し、NewYork証券取引所に上場しました。 Symbolics社では、HardwareだけでなくOperating Systemから開発ツール、アプリケーションソフトウェアまで開発を行っていた。会社の基本コンセプトは、"Software First" 最初にソフトウェアありき。Hardwareは、ソフトウェアを実行するために設計されるべきだという考えのもと、Operating SystemからObject Oriented Programing Modelで設計されており、それを現実的な速度で実行するためのCPUを設計していた。特徴的な機能は、実行時の型チェックとその結果に応じた関数呼び出しや、型変換を行うことと、高速なメッセージパッシングのための専用のキャッシュを装備していた。

オブジェクト指向言語として、Zatalispの拡張となるFlavorsが当初より実装されていた。特徴としては、多重継承機能。その後、CommonLispの制定後、CommonLispの拡張としてCLOS(CommonLisp Object System)が制定された。それに伴い、SymbolicsCommonLispの拡張としてCLOS互換のNewFlavorsが提供されるようになった。またこのCommonLispへの移行に伴い、OSもGeneraと命名された。NewFlavorsの特徴ひとつは、Generic Fucntionである。Lisp関数とObjectのメソッド呼び出しを同一のフォーマットとして、引数の型によって最適な呼び出しを実行時に選択していた。

もっとも大規模なアプリケーションとして、3D Computer Graphics の製作システムがあった。このアニメーションシステムは、MITでのActor理論をベースに開発されていた。また形状モデリングソフトウェアも、Object Oriented Programing Modelで記述されており、多重継承を非常にうまく実装していた。3DCGの製作環境では実行速度が重視されるため、LispですがSillicon Graphics社のUNIXワークステーション上のC言語で記述されたシステムに、劣らないパフォーマンスを実現していた。

Symbolicsの環境の機能とともに、それらから感じられたメリット及び欠点などを紹介していく。

Machintosh IIFXにSymbolicsのIvoryカードを搭載したもので、Symbolics Generaの実機デモを行う予定です。 ただし20年前の機材なので、動作しない場合はご了承ください。

講演者の略歴

経歴

職務略歴

86-92 日本シンボリック株式会社
  • 各種 3DCG データ・コンバーター開発、およびビデオ機器制御ソフトウェア開発
  • NHK 人体プロジェクト 3DCG ツール開発およびプロダクション・サポート
  • NHK シンセビジョン・プロジェクト HDTVによるバーチャルスタジオ
  • ソニー Hi-Vision Video Library オープニングCG製作
  • ソニー System-G (リアルタイム3Dビデオエフェクター) 制御プログラムおよびデモシーケンス開発
  • TBS ハイビジョン「万里の長城」オープニングCG製作サポート
  • テレビ朝日 ハイビジョン「あの日に戻りたい」 特撮CG製作サポート
  • フジテレビ 各種データ・コンバーター開発
  • 日本テレビ 天気予報自動作画システム設計および開発
  • 他 各種3DCG製作サポート
93-95 ニチメングラフィックス株式会社(日本シンボリックスより社名変更)
  • ソニー プレイステーション向け3Dコンテンツ制作ツール開発
  • 任天堂 各種3Dコンテンツ制作用ツール開発
95-02 株式会社スクウェア
  • 技術デモ「ファイナルファンタジー6 in 3D on SGI Onyx」開発 '95 SIGGRAPH
  • 「ファイナルファンタジー 7」 CG スーパーバイザー
  • 技術デモ プレイステーション2 発表会向けデモ 開発
  • 技術デモ ソニー GS–Cube 「ファイナルファンタジー the Movie」リアルタイム・レンダリング '00 SIGGRAPH
  • 映画「ファイナルファンタジー The Spirits Within」R&D スーパーバイザー
02-06 米国エレクトロニック・アーツ
  • 次世代機向け技術基盤設計と開発支援
  • Playstation3発表デモ開発支援
06-12 Avatar Reality社
  • 起業、戦略立案、資金調達
  • 高品位バーチャルワールド BlueMars設計及び開発統括
  • BlueMars Mobile、BlueMars Lite開発

招待講演2: A New Foundation for C/C++: Formal Semantics and Compilation Validation for LLVM Compiler

Chung-Kil Hur (Seoul National University)

Hur氏の写真

概要

My long-term research goal is to establish a solid foundation for the C/C++ language, which requires a "simple" semantics of C/C++ and a "correct" compiler. For this, we will develop (i) a simple formal semantics of C supporting all practically used features such as integer-pointer casts; and (ii) a verified translation validator for the full LLVM compiler. Achieving both (i) and (ii) is not particularly easy because a simple semantics usually fails to justify many compiler optimizations.

In this talk, I will give a high-level introduction to our project including many technical problems that arise on the way. Then, I will present our solutions to two of the problems. One is to give a simple memory model that supports integer-pointer casts, yet still justify most of the existing compiler optimizations. The other is to give a new reasoning principle for coinduction that does not require any syntactic guardedness checking. We formalized this theory as Paco library for Coq, which made our coinductive reasoning for compilation validation a lot easier.

講演者の略歴

Chung-Kil Hur is an assistant professor in Department of Computer Science and Engineering at Seoul National University. Previously he worked as a postdoctoral researcher at Microsoft Research Cambridge, Max Planck Institute for Software Systems (MPI-SWS) and Laboratoire PPS. He obtained a Ph.D. from University of Cambridge and a B.Sc. in Computer Science and in Mathematics from Korea Advanced Institute of Science and Technology (KAIST). He also received a bronze medal in the 35th International Mathematical Olympiad (IMO) in 1994. His research interests are in software verification, interactive theorem proving, probabilistic programming and Beyesian inference.