کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
10329284 | 685348 | 2005 | 13 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Cobalt: A Language for Writing Provably-Sound Compiler Optimizations
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
![عکس صفحه اول مقاله: Cobalt: A Language for Writing Provably-Sound Compiler Optimizations Cobalt: A Language for Writing Provably-Sound Compiler Optimizations](/preview/png/10329284.png)
چکیده انگلیسی
We overview the current status and future directions of the Cobalt project. Cobalt is a domain-specific language for implementing compiler optimizations as guarded rewrite rules. Cobalt optimizations operate over a C-like intermediate representation including unstructured control flow, pointers to local variables and dynamically allocated memory, and recursive procedures. The design of Cobalt engenders a natural inductive strategy for proving the soundness of optimizations. This strategy is fully automated by requiring an automatic theorem prover to discharge a small set of simple proof obligations for each optimization. We have written a variety of forward and backward intraprocedural dataflow optimizations in Cobalt, including constant propagation and folding, branch folding, full and partial redundancy elimination, full and partial dead assignment elimination, and simple forms of points-to analysis. The implementation of our soundness-checking strategy employs the Simplify automatic theorem prover, and we have used this implementation to automatically prove the above optimizations correct. An execution engine for Cobalt optimizations is implemented as part of the Whirlwind compiler infrastructure.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 132, Issue 1, 30 May 2005, Pages 5-17
Journal: Electronic Notes in Theoretical Computer Science - Volume 132, Issue 1, 30 May 2005, Pages 5-17
نویسندگان
Sorin Lerner, Todd Millstein, Craig Chambers,