The post has been translated automatically. Original language: Russian
In previous articles, we went through almost the entire computing chain.:
program
, the compiler
, operating system
↓
command architecture
↓
processor
↓
digital logicAt each level, you can formulate properties and try to prove that the implementation corresponds to them.
A natural question arises:
is it possible to combine all this and build a computer whose correctness has been fully proven?
Answer: to a large extent, yes.
But the word "whole" requires caution.
The proof can be built as a chain
Let's imagine a program for which it is proved:
the program
conforms
to the specificationThen you need to prove that the compiler preserves its behavior.:
the source code
, machine codeNext— that the operating system provides the conditions that the program expects.:
isolation
memory
access rights
processesThe next level is the processor architecture:
machine instructions
, expected state changeAfter that, the processor implementation is checked.:
ISA specification
↓
RTLThus, it is possible to build a long chain of correspondences.:
requirement
↓
program
, the compiler
↓
OS
↓
ISA
↓
RTL
↓
logic diagramIf each transition is proven, the number of components that simply have to be trusted decreases dramatically.
This is almost the entire computer.
You can really go very far at the digital level.
You can check:
- programs;
- libraries;
- compilers;
- operating system kernels;
- protocols;
- team architectures;
- processor blocks;
- memory controllers;
- device interfaces;
- RTL;
- matching different levels of digital implementation.
Ideally, a system is obtained where each next level is formally linked to the previous one.
The main idea here is not that each component is individually marked "tested".
Something else is important:
The evidence must be interconnected.
If the program is proven with respect to one processor model, and the real processor implements another, the chain is broken.
Where does math end?
After the digital logic, the physical device begins.
RTL
↓
logic gates
↓
transistors
↓
crystal
, a real computerAnd here there are factors that can no longer be reduced solely to the logical behavior of the program or processor.
For example:
- manufacturing defects;
- unstable nutrition;
- overheating;
- radiation;
- electromagnetic interference;
- aging of components;
- physical damage.
It can be mathematically proved that a certain digital circuit behaves correctly under given conditions.
But you can't automatically conclude from this:
a specific physical instance will never fail.
This is a different class of tasks.
So a fully proven computer is impossible?
It depends on what counts as "completely".
If we are talking about the digital behavior of a computing system relative to a formal model, we can build a very deep chain of evidence.
If it is required to prove:
This physical computer
will never, under any circumstances
, make a mistake.such a statement is practically meaningless.
The physical world is not a perfect mathematical model.
Therefore, it is more correct to speak not about absolute infallibility, but about the limit of proof.
For example:
proven:
digital behavior of the system
assumed:
correct operation of physical electronicsThe lower this limit is, the stronger the guarantee of the entire system.
Physical risk can also be reduced.
Formal verification does not end because nothing further can be done.
It's just that the methods are changing.
For the physical layer, the following are applied:
- production testing;
- reservation;
- memory error control;
- power control;
- temperature monitoring;
- watchdog mechanisms;
- duplication of calculations;
- error detection and correction;
- fault-tolerant architectures.
That is, the system can combine:
formal proofs
+
hardware diagnostics
+
fault toleranceFormal verification answers the question:
Is the system designed correctly?
And reliability methods answer another question.:
what happens if the physical device fails?
Verifiability needs to be designed in advance
An important conclusion follows from the whole series.
Formal verification is not only the verification stage of the finished product.
It affects the architecture of the system itself.
If provability is required, it is usually advantageous:
- a small number of states;
- simple interfaces;
- clear component boundaries;
- minimum trusted base;
- deterministic behavior;
- a simple memory model;
- the minimum amount of hidden logic.
Therefore, an architecture designed for maximum performance and an architecture designed for maximum verifiability may look completely different.
Sometimes you have to choose:
more complexity
and performanceor
less complexity
and stronger evidenceThis is no longer a question of a verification tool.
It's an architectural choice.
From the program to the processor
At the beginning of the series, we asked a simple question:
Why is there not enough testing?
Now the chain looks much wider.
Specification
↓
program
, the compiler
, operating system
, team architecture
↓
processor
, digital logic
, physical deviceAt each level, you can either simply trust the system, or try to reduce the area of trust with the help of evidence.
Therefore, the most accurate goal does not look like this:
to build a computer in which no mistakes are possible.
And so:
to build a computing system in which the maximum possible part of the behavior is formally defined and proven.
This is a fundamentally different approach to the development of computing systems.
Do not first create the most complex system possible, and then look for errors in it.
And initially design it so that the key properties can be proved.
This may be the next stage in the development of systems where the cost of error is too high to be limited to testing alone.
В предыдущих статьях мы прошли почти всю вычислительную цепочку:
программа
↓
компилятор
↓
операционная система
↓
архитектура команд
↓
процессор
↓
цифровая логикаНа каждом уровне можно формулировать свойства и пытаться доказать, что реализация им соответствует.
Возникает естественный вопрос:
можно ли объединить всё это и построить компьютер, правильность которого доказана целиком?
Ответ: в значительной степени — да.
Но слово «целиком» требует осторожности.
Доказательство можно строить как цепочку
Представим программу, для которой доказано:
программа
соответствует
спецификацииЗатем нужно доказать, что компилятор сохраняет её поведение:
исходный код
↓
машинный кодДалее — что операционная система обеспечивает условия, на которые рассчитывает программа:
изоляция
память
права доступа
процессыСледующий уровень — архитектура процессора:
машинная инструкция
↓
ожидаемое изменение состоянияПосле этого проверяется реализация процессора:
спецификация ISA
↓
RTLТаким образом можно построить длинную цепочку соответствий:
требование
↓
программа
↓
компилятор
↓
ОС
↓
ISA
↓
RTL
↓
логическая схемаЕсли каждый переход доказан, количество компонентов, которым приходится просто доверять, резко уменьшается.
Это уже почти весь компьютер
На цифровом уровне действительно можно зайти очень далеко.
Можно проверять:
- программы;
- библиотеки;
- компиляторы;
- ядра операционных систем;
- протоколы;
- архитектуры команд;
- процессорные блоки;
- контроллеры памяти;
- интерфейсы устройств;
- RTL;
- соответствие различных уровней цифровой реализации.
В идеальном случае получается система, где каждый следующий уровень формально связан с предыдущим.
Главная идея здесь не в том, что каждый компонент отдельно получил отметку «проверено».
Важно другое:
доказательства должны соединяться между собой.
Если программа доказана относительно одной модели процессора, а реальный процессор реализует другую, цепочка разрывается.
Где заканчивается математика
После цифровой логики начинается физическое устройство.
RTL
↓
логические элементы
↓
транзисторы
↓
кристалл
↓
реальный компьютерИ здесь появляются факторы, которые уже нельзя свести только к логическому поведению программы или процессора.
Например:
- дефекты производства;
- нестабильное питание;
- перегрев;
- радиация;
- электромагнитные помехи;
- старение компонентов;
- физическое повреждение.
Можно математически доказать, что определённая цифровая схема при заданных условиях ведёт себя правильно.
Но нельзя из этого автоматически заключить:
конкретный физический экземпляр никогда не даст сбой.
Это уже другой класс задач.
Значит, полностью доказанный компьютер невозможен?
Зависит от того, что считать «полностью».
Если речь идёт о цифровом поведении вычислительной системы относительно формальной модели, можно построить очень глубокую цепочку доказательств.
Если же требуется доказать:
этот физический компьютер
никогда и ни при каких условиях
не ошибётсятакое утверждение практически бессмысленно.
Физический мир не является идеальной математической моделью.
Поэтому правильнее говорить не об абсолютной безошибочности, а о границе доказательства.
Например:
доказано:
цифровое поведение системы
предполагается:
корректная работа физической электроникиЧем ниже находится эта граница, тем сильнее гарантия всей системы.
Можно уменьшать и физический риск
Формальная верификация заканчивается не потому, что дальше ничего нельзя сделать.
Просто меняются методы.
Для физического уровня применяются:
- производственное тестирование;
- резервирование;
- контроль ошибок памяти;
- контроль питания;
- температурный мониторинг;
- watchdog-механизмы;
- дублирование вычислений;
- обнаружение и коррекция ошибок;
- отказоустойчивые архитектуры.
То есть система может сочетать:
формальные доказательства
+
аппаратную диагностику
+
отказоустойчивостьФормальная верификация отвечает на вопрос:
правильно ли спроектирована система?
А методы надёжности отвечают на другой:
что произойдёт, если физическое устройство всё-таки даст сбой?
Верифицируемость нужно проектировать заранее
Из всей серии следует важный вывод.
Формальная верификация — это не только этап проверки готового продукта.
Она влияет на архитектуру самой системы.
Если требуется доказуемость, обычно выгодны:
- небольшое количество состояний;
- простые интерфейсы;
- чёткие границы компонентов;
- минимальная доверенная база;
- детерминированное поведение;
- простая модель памяти;
- минимальное количество скрытой логики.
Поэтому архитектура, созданная для максимальной производительности, и архитектура, созданная для максимальной верифицируемости, могут выглядеть совершенно по-разному.
Иногда приходится выбирать:
больше сложности
и производительностиили
меньше сложности
и сильнее доказательстваЭто уже не вопрос инструмента верификации.
Это архитектурный выбор.
От программы до процессора
В начале серии мы задавали простой вопрос:
почему недостаточно тестирования?
Теперь цепочка выглядит гораздо шире.
спецификация
↓
программа
↓
компилятор
↓
операционная система
↓
архитектура команд
↓
процессор
↓
цифровая логика
↓
физическое устройствоНа каждом уровне можно либо просто доверять системе, либо пытаться уменьшить область доверия с помощью доказательств.
Поэтому наиболее точная цель выглядит не так:
построить компьютер, в котором невозможно ни одной ошибки.
А так:
построить вычислительную систему, в которой максимально возможная часть поведения формально определена и доказана.
Это принципиально другой подход к разработке вычислительных систем.
Не сначала создать максимально сложную систему, а потом искать в ней ошибки.
А изначально проектировать её так, чтобы ключевые свойства можно было доказать.
Именно в этом может заключаться следующий этап развития систем, где цена ошибки слишком высока, чтобы ограничиваться только тестированием.
Share
