При HPC операциите има неизбежен компромис между скорост и надеждност
(снимка: CC0 Public Domain)
Високопроизводителните изчисления (HPC) са необходими за непрекъснато нарастващия брой задачи – като обработка на изображения или различни приложения за т.нар. „дълбоко самообучение” в невронни мрежи. Това са задачи, при които трябва да се претърсят огромни купища данни и това да стане сравнително бързо, в противен случай изпълнението им може да отнеме неоправдано време.
Широко разпространено е мнението, че при извършване на операции от този вид има неизбежен компромис между скорост и надеждност. Ако скоростта е основен приоритет, то надеждността вероятно ще пострада – и обратно. Екип изследователи от Масачузетския технологичен институт поставя това понятие под въпрос. Учените твърдят, че всъщност можем да имаме и двете.
С новия език за програмиране, който учените са написали специално за високопроизводителни изчисления, „скоростта и коректността не се конкурират. Вместо това те могат да вървят заедно, ръка за ръка, в програмите”, казва Аманда Лиу, втора година докторант в Лабораторията по компютърни науки и изкуствен интелект (CSAIL) на Масачузетския технологичен институт.
Лиу и нейните колеги описаха потенциала на своето наскоро разработено творение, т. ар. „тензорен език” (ATL), миналия месец на конференцията „Принципи на езиците за програмиране”, съобщи SciTechDaily.
Основната обосновка на ATL е следната: „Като се има предвид, че високопроизводителните изчисления са толкова ресурсоемки, вие искате да можете да модифицирате или пренаписвате програмите в оптимална форма, за да ускорите изчисленията. Човек често започва с програма, която е най-лесна за писане, но това може да не е най-бързият начин да я стартирате, така че все още са необходими допълнителни корекции”.
Но как се разбира кой е най-добрият начин? За да се постигне идеалната оптимизация на кода, се разчита на нещо, известно като „помощник за доказване”. За тази цел новият език се основава на съществуващ език, Coq, който съдържа въпросния „помощник за доказване”. Помощникът, от своя страна, има присъщата способност да доказва своите твърдения по математически строг начин.
Coq има и друга присъща характеристика, която го прави привлекателен: програмите, написани с него, или адаптациите му, винаги се прекратяват и не могат да работят вечно в безкрайни цикли. „Изпълняваме програма, за да получим единичен отговор – число или тензор”, пояснява Лиу. „Програма, която никога не се прекратява, би била безполезна за нас”.
Засега това е първият и единствен тензорен език с официално проверени оптимизации. Лиу предупреждава обаче, че ATL все още е само прототип. Макар и обещаващ, той все още не е напълно доказан.