Группа исследователей под руководством доцента кафедры электротехники, вычислительной техники и компьютерных наук Университета Карнеги-Меллона, Брайана Парно опубликовала новый язык программирования Armada. Язык предназначен для формальной проверки высокопроизводительных параллельных программ.
Armada
Безопасно писать высокопроизводительные параллельные программы очень сложно. «Когда у вас одновременно происходит несколько событий, вам нужен какой-то способ управления ими, чтобы убедиться, что эти процессы не мешали друг другу», – говорит Брайан Парно.
Новый язык программирования используется для высокопроизводительных параллельных вычислений и гарантирует, что написанные на нем программы корректны, и это можно доказать математически.
Язык и инструмент под названием Armada были представлены в этом году на конференции по разработке и реализации языков программирования и получили награду Distinguished Paper.
Проверка для программиста
Ранее для проверки текста в текстовом редакторе на орфографические ошибки, люди специально сообщали программе о необходимости начать эту процедуру, кликнув на функции «Проверка орфографии». Проверка занимала несколько секунд, после чего пользователи могли исправить свои опечатки.
В настоящее время проверка орфографии выполняется автоматически. Постоянная проверка орфографии является примером «параллельного» программирования, в котором исполняемый файл выполняется одновременно с другими программами и вычислениями.
Большинство программ сегодня представляют собой параллельные, – начиная с операционных систем и заканчивая множеством приложений: от обработки текста до просмотра веб-страниц.
«Armada разработана чрезвычайно гибкой, чтобы код было удобно писать каждому разработчику, и он работал как можно быстрее», – говорит Парно. «Но при этом программисты будут твердо уверены в том, что код будет правильно исполняться и ничего не испортит».
Возможности и перспективы
Благодаря C-подобному языку и семантике на основе конечного автомата с малым шагом, Armada дает разработчикам возможность произвольной компоновки памяти и примитивов синхронизации.
Чтобы «облегчить жизнь» разработчиков, Armada использует автоматизацию на базе SMT (satisfiability modulo theories) – задача разрешимости для логических формул с учётом лежащих в их основе теорий. А также библиотеку мощных методов рассуждений, включая гарантию на соответствие, обеспечение TSO (Total Store Order), сокращение и анализ псевдонимов. TSO – полностью упорядоченный доступ, когда процессор гарантирует, что операции доступа к памяти будут обращаться к основному ОЗУ в точности в том порядке, в котором закодированы.
Все эти техники доказали свою надежность, и со временем Armada может быть существенно расширена с помощью дополнительных стратегий. По заявлению разработчиков, используя Armada, можно достичь производительности, эквивалентной производительности непроверенного кода.
Парно считает, что Armada принесет пользу любому, кто пишет параллельные программы, охватывающие огромное количество приложений. «От систем начисления заработной платы до больничных записей и любого вида электронной коммерции – все они поддерживаются базами данных, а базы данных всегда будут поддерживаться параллельным программным обеспечением», – говорит Парно. «Помимо простых программ, в наши дни почти все имеет отношение к параллелизму».
