Новый фреймворк формализует оригинальные техники программирования

Два года назад группа исследователей Лаборатории компьютерных наук и искусственного интеллекта (Computer Science and Artificial Intelligence Laboratory) Массачусетского технологического института (МТИ) предложила необычный способ повышения эффективности процедуры вычислений: путем исключения отдельных шагов. И хотя ученые представили разные практические варианты применения технологии, ее применение на практике не пошло — разработчики неохотно обращаются к методам, которые им не до конца понятны.

Один из способов значительно повысить производительность за счет небольшого уменьшения точности вычислений — перфорация циклов. Кроме того, имеются высокоскоростные «неточные» чипы, где вместо булевой логики для обработки инструкций схемы применяются вероятностные методы, а также экономичные схемы памяти, которые не гарантируют абсолютную точность хранения. Все эти разработки объединяет одно: скептицизм со стороны инженеров, которые опасаются, что неточность компьютерных схем может привести к катастрофическим ошибкам на выходе системы.

На конференции Programming Language Design and Implementation, организованной Association for Computing Machinery, которая пройдет в 11-16 июня 2012 г. в Пекине (Китай), группа ученых под руководством Мартина Ренара (Martin Rinard) намерена представить новый математический фреймворк, который позволит убедить разработчиков в эффективности неточных вычислений. Эта система выполняет соответствующие расчеты и гарантирует: если исходная программа работает нормально, аналогично будет себя вести и ускоренная ее версия, построенная с применением неточных вычислений. Для построения своей системы ученые использовали технологии верификации, применяемые в разработке аппаратных средств, академические работы в области теории алгоритмов и методики, применяемые для создания критически важного ПО с большой ценой ошибки.

Новый инструмент автоматической верификации предоставит разработчикам возможность разобраться с тем, какие процедуры можно модернизировать, в каких фрагментах имеет смысл использовать перфорацию цикла или другие методы ускорения работы.