Обсуждение

Хм, по-моему, заявлять, что в твоей ОС нет багов - все равно, что заявлять, что в производимым тобой автомобиле ничего и никогда не сломается...

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

Очепяточтка. Хотел написать: В данном случае, "нет багов" *означает что* есть формальное доказательство их отсутствия.

Забавно, мы как раз вчера обсуждали написание безбажной ОС и браузера. Я отметил, что гении сейчас вполне могут такие писать :). Но я правда на других примерах верификации основыввался (верифицированные компиляторы, языки с депендент тайпс и т.д.). Вобщем, молодцы австралийцы, там тоже есть гении :).

Ребята из ERTOS потратили 2 человеко-года на написание Haskell-прототипа, и 2 человеко-месяца на переписывание его на С. И затем грохнули 20 человеко-лет на доказательство правильности кода -- 11 человеко-лет на само доказательство и 9 человеко-лет на инструментарий для этого доказательства. Т.е. стоимость "доказанного кода" идет к стоимости "недоказанного кода" примерно как 10:1). А вот тут они не совсем передовые, потому как последние достижения позволяют говорить о том, что оверхед для верификации будет небольшой, сравнимым с размером кода. Правда, надо использовать специальные наработки. Тут тоже своя инженерия есть - инженерия доказательств :).

Очень интересный жизненный цикл получения этого кода (сам код на C, но прототип на Haskell. У меня складывается, что написание сразу двух эквивалентных программ на двух разных языках является сейчас магистральным направлением для хорошо верифицированных и надежных программ -- тот же Harold Lawson употребил этот прием для архитектуры Cy-Clone, коды которой писал на ассемблере, а исполнимые комментарии на чем-то типа Паскаля, а затем добивался одинакового исполнения кодов и комментариев -- "для проверки" Для верифицированных даже поболее двух :). Целевой язык, язык спецификации, язык для автоматизации доказательств. В идеале, реализацию можно извлечь из конструктивного доказательства корректности спецификации.

сам код на C, но прототип на Haskell. У меня складывается, что написание сразу двух эквивалентных программ на двух разных языках является сейчас магистральным направлением для хорошо верифицированных и надежных программ Они еще отмечают, что благодаря написанию прототипа на Хаскеле, общее время создания ядра значительно сократилась в сравнении с другими аналогичными проектами.

Дык, про Фантом вроде как зимой прошлой волна по миру прошлась? А вообще, чем больше я думаю про идею DZ, тем больше у меня складывается впечатление, что необходимо строить собственную хардварную архитектуру под эту ОС... Есть ощущение, что по итогу это сэкономит много сил. Но это только мое ощущение.

Нет, это только моё ощущение про хардверную архитектуру для этой ОС! :) Например, я писал (ровно год назад, http://ailev.livejournal.com/620515.html): А дальше MRAM планирует стать самой быстрой памятью, с сохранением всех своих достоинств: http://www.mram-info.com/researchers-germany-have-built-spin-torque-system-dramatically-faster-any-other -- 1нс, в то время как текущий процессорный цикл сейчас 1.5нс, а DRAM имеет цикл 30нс. Это означает, что на подходе совсем новые компьютерные архитектуры: не только без внешнего диска (эта память сама себе диск -- она энергонезависима), но и без процессорного кэша (эта память и так достаточно быстра). Эксперименты уже вовсю идут (http://techon.nikkeibp.co.jp/english/NEWS_EN/20080827/156977/). Насчет "мировой волны", так была пара заметок в первых числах февраля 2009, и все после этого заглохло. Но то, что у проекта есть своя англоязычная страничка -- это очень хорошо.

написание сразу двух эквивалентных программ И даже не обязательно программ. Можно дополнить программу неисполнимыми спецификациями (например, пред- и постусловиями) и получить аналогичный результат. Даже лучше, чтобы использовались различные парадигмы - процедурный и функциональный языки, язык программирования и неисполнимые спецификации. В одной парадигме проще делать одинаковые ошибки. добивался одинакового исполнения кодов и комментариев На всякий случай - тестирование не доказывает эквивалентности. Надо еще почитать, а как они доказали, что в Haskell прототипе нет багов :)

Это замечательное достижение, но, думаю, что надо сказать про сам проект микроядра L4, центр разработки которого в Германии. Автралийцы осуществили верификацию модифицированной версии этого ядра. А вот то, что проект L4 до некоторых пор был почти не американским -- важно. Ситуация, впрочем, уже меняется.

Я вообще как-то чувствую тренд на перемещение центра мирового программирования куда-то поближе к Европе. Вчера вот слушал рассказ про самый навороченный в мире САПР -- так было непонятно сразу, то ли это французский язык, то ли английский у докладчика...

Я все надеюсь, но пока не чувствую, увы.

Наверное, я чувствую именно потому, что не надеюсь :)

Но то что в каждой интересной команде есть хотя бы один русскоговорящий -- это уже железно года два как происходит.

Мы тут подумывали поставить MRAM в один из проектов (а ля быстрая и надежная флэш), увы, реально можно купить не более 4 Mbit, да и дороговато получается. Но конечно именно для Фантома стоило бы ее использовать, если и не под всю оперативную память, то хотя б под ядро.

У верификационного софта центр скорее во Франции/Германии. Хотя Англия/США нельзя сказать что отстают.

Samsung уже начал производить PRAM на 512Mb -- http://www.mram-info.com/samsungs-has-started-produce-512mb-phase-change-memory (скорость в 7 раз быстрей NOR Flash).

Любопытно, хотя наши разработчики стараются не связываться с самсунгом. Наши изделия выпускаются малыми партиями но годами, поэтому срок жизни чипов на производстве имеет важное значение. А то бывало года 3-4 пройдет и не найти уже старых микросхем, а остатки распродают по десятикратной цене. В этом отношении freescale-motorola, например, гораздо надежнее.

По крайней мере в тех областях, с которыми мне приходится сталкиваться, software engineering в Европе уже зарулил штаты по полной программе.