Algebra-dynamic models for program parallelization
Abstract
We propose algebra-dynamic models and a method for checking correctness of optimizing transformations for multithread programs and programs for graphical processing units. Proposed models are used together with rewriting rules technique to prove correctness of transformations and increase effectiveness of program parallelization.
Problems in programming 2010; 1: 39-55
Full Text:
PDF (Русский)References
Akhter S., Roberts J. Multi-Core Programming. Increasing Performance through Software Multi-threading. – Intel Press, 2006. – 336 p.
General-Purpose Computation Using Graphics Hardware. http://www.gpgpu. Org .
Дорошенко А.Е., Жереб К.А., Яценко Е.А. Формализованное проектирование эффективных многопоточных программ // Проблеми програмування. – 2007. – № 1. – С. 17–30.
Дорошенко А.Е., Жереб К.А., Яценко Е.А. Об оценке сложности и координации вычислений в многопоточных программах // Проблеми програмування. – 2007. – № 2. – С. 41–55.
Дорошенко А.Е., Жереб К.А. Разработка высокопараллельных приложений для графических ускорителей с использованием переписывающих правил // Проблеми програмування. – 2009. – № 3. – С. 3–18.
Doroshenko A., Shevchenko R. A Rewriting Framework for Rule-Based Programming Dynamic Applications, Fundamenta Informaticae. – 2006. – Vol. 72, N 1–3. –P. 95–108.
TermWare. – http://www.gradsoft.com.ua/ products/termware_rus.html . 8. Дорошенко А.Е., Шевченко Р.С. Система символьных вычислений для программирования динамических приложений // Проблеми програмування. – 2005. – № 4. – С. 718–727.
Андон Ф.И., Дорошенко А.Е., Цейтлин Г.Е., Яценко Е.А. Алгеброалгоритмические модели и методы параллельного программирования. – Киев: Академпериодика, 2007. – 631 с.
Kundu S., Tatlock Z., and Lerner S. Proving optimizations correct using parameterized program equivalence. In Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation (Dublin, Ireland, June 15–21, 2009). PLDI '09. – P. 327–337.
Lerner S., Millstein T., and Chambers C. Automatically proving the correctness of compiler optimizations. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (San Diego, California, USA, June 09– 11, 2003). PLDI '03. – P. 220–231.
Lerner S., Millstein T., Rice E., and Chambers C. Automated soundness proofs for dataflow analyses and transformations via local rules. SIGPLAN Not. – 2005. – Vol. 40, N 1. – P. 364–377.
Lacey D., Jones N. D., Van Wyk E., and Frederiksen C. C. Proving correctness of compiler optimizations by temporal logic. In Proceedings of the 29th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (Portland, Oregon, January 16–18, 2002). POPL '02. – P. 283–294.
Leroy X. Formal certification of a compiler back-end or programming a compiler with a proof assistant. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Charleston, South Carolina, USA, January 11–13, 2006). POPL '06. – P. 42–54.
Farzan A., Chen F., Meseguer J., and Rosu G. Formal Analysis of Java Programs in JavaFAN. In Int. Conf. on Computer Aided Verification, Boston, Mass., 2004.
Timothy Winkler, “Programming in OBJ and Maude”, in Functional Programming, Concurrency, Simulation and Automated Reasoning, International Lecture Series 1991–1992, Springer-Verlag, McMaster University, Hamilton, Ontario, Canada, 1993. – P. 229–277.
NVidia CUDA technology. http://www. nvidia.com/cuda .
Conway’s Game of Life http://en.wikipedia.org/wiki/Conway %27s_Game_of_Life.
Дорошенко А.Е., Жереб К.А. Автоматизация разработки приложений для графических ускорителей с использованием переписывающих правил // Труды 5 Восточно-европейской научно-практической конференции по программной инженерии CEE-SECR 2009. – Москва, 28–29 октября 2009.
Refbacks
- There are currently no refbacks.