Study on a simple and flexible type system for relaxed memory consistency models
| Project/Area Number |
25730050
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Institute of Physical and Chemical Research |
|---|
Principal Investigator |
Maeda Toshiyuki 国立研究開発法人理化学研究所, 計算科学研究機構, チームリーダー (50436557)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Project Status |
Completed (Fiscal Year 2015)
|
| Budget Amount *help |
¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
Fiscal Year 2014: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2013: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
|
|---|
| Keywords | メモリ一貫性モデル / 型システム / プログラム検証 / プログラミング言語 |
|---|
| Outline of Final Research Achievements |
We designed a program verification method that is able to verify correctness of program behavior (in this research, the memory safety that ensures that programs perform no illegal memory operation) under various memory consistency models, especially under the relaxed ones (where the results of program execution may not match any result that can be obtained from executing multiple programs in a sequential and interleaved manner), which are one of the causes of mistakes in parallel programming. More specifically, we designed a simple and unified type system of a programming language that is able to handle various memory consistency models that may vary from CPU to CPU, and programming language to programming language (the conventional approaches were impractical in the sense that different verification methods have to be designed for each memory consistency model).
|
Report
(4 results)
Research Products
(5 results)
