автореферат диссертации по , 05.00.00, диссертация на тему:Формальная верификация процессора с устройствами поддержки виртуальной памяти

1 Введение

1.1 Используемые обозначения.

1.2 Среда формальных доказательств PVS.

1.3 Базовые логические элементы

1.4 Виртуальная память.

1.5 Декомпозиция доказательства

1.5.1 Уровень интерфейса памяти

1.5.2 Уровень интерфейса процессора.

2 Блок поддержки виртуальной памяти

2.1 Спецификация MMU

2.1.1 Допущение для MMU.

2.1.2 Гарантии MMU.

2.2 Дизайн MMU.

2.3 Корректность MMU.

3 VAMP с поддержкой виртуальной памяти

3.1 Спецификация VAMP процессора.

3.2 Имплементация процессора VAMP.

3.2.1 Алгоритм Томасуло

3.2.2 Дизайн процессора VAMP.

3.2.3 Имплементация блока памяти процессора VAMP

3.3 Критерий корректности.

3.3.1 Планировочные функции.

3.3.2 Инвариант корректности

3.3.3 Обзор доказательства.

3.4 Корректность между прерываниями.

3.4.1 Корректность блока памяти при чтении / записи

3.4.2 Выборка инструкций.

3.5 Корректность с прерываниями.

3.5.1 Полная корректность

На текущий момент, существует много приложений где процессора используются в устройствах, критичных для жизни человека, например атомные электрические станции, самолеты, поезда, автомобили или медицинские приборы. Разработчики процессоров используют различные тесты для того чтобы обнаружить ошибки в них. Так как не исчерпывающие тесты пе покрывают все возможные случаи поведения процессора, процессора выпускаемые индустрией могут содержать ошибки. Формальная верификация все больше и больше признается единственной альтернативой, так как актуальные результаты в формальной верификации эквивалентны симуляции всех возможных случаев поведения процессора. Более того, это даже лучше чем симуляция потому, что можно получить корректность нескольких модулей сразу.В данной работе доказывается только корректность работы аппаратного обеспечения используемого в академической системе проекта Verisoft. Следует отметить, что ошибки программного обеспечения также могут быть причиной неправильного поведения системы. Поэтому, как доказательство корректности работы апнаратного уровня, так и доказательство корректности программного обеспечения необходимы, а доказательство корректности работы аппаратного уровня это только первый шаг на пути получения корректности полной компьютерной системы.К р а т к о е с о д е р ж а н и е глав В главе 1 рассматривается основная нотация, используемая во всей работе. Так же будут рассмотрены: система формальных доказательств, виртуальная память и основной подход к декомпозиции доказательств в данной работе.В главе 2 рассматривается конструкция неоптимизированного блока поддержки виртуальной памяти (ММи), который является аппаратной частью поддержки виртуальной памяти. Здесь же будет доказана корректность работы данного блока при нетривиальных условиях: данные в ячейках памяти И используемые для транслирования адреса не должны быть перезаписаны в течении всего запроса к MMU.В последней главе 4 обобпдаются результаты, проводится дискуссия о достоинствах и недостатках разработанной системы, представляется информация о работах других ученый в данном направлении, а также обсуждаются возможности для дальнейшей работы.

Заключение

4.1 Итоги

В данной работе докладывается о формальной верификации сложного процессора, поддерживающего трансляцию адреса и внешние прерывания. Эта работа была основана на следующих предыдущих работах: не формальном доказательстве корректности блока управления виртуальной памятью [НП05], формальной верификации алгоритма Томасуло [KrôOl] и формальной верификации процессора VAMP без трансляции адреса [ВеуОб]. Процессор VAMP является 32-битным RISC процессором с планировщиком Томасуло, блоком памяти с интерфейсом между кэшем и памятью, блоком для вычислений с фиксированной запятой и тремя блоками для вычислений с плавающей запятой. Результат данной работы опубликован в [DHP05].

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

Следующим шагом, MMU был интегрирован в блок памяти процессора VAMP [ВеуОб,KrôOl, JK00,BBJ+02,BJK+03,BJK+05,Jac02a] один для трансляции адреса при чтении/записи и один в стадию выборки инструкции для трансляции адреса при выборке инструкции.

В дополнение к имплементации, также была разработана модель программиста процессора VAMP, которая была использована как специфика

Номер Название теории Кол-во команд Кол-во лемм

1 Основные схемы 5505 134

2 АЛУ 2202 76

3 Конвейеризированный DLX 1850 53

4 Алгоритм Томасуло 5847 186

5 VAMP без MMU (без алгор. Томасуло) 24753 495

6 Локальное MMU 7399 85

7 VAMP с MMU (без алгор. Томасуло) 36785 587

1. BCBZ02. S. Berezin, E. Clarke, A. Biere, and Y. Zhu. Verification of out-of-order processor designs using model checking and a lightweight completion function. In Formal Methods in System Design, volume 20, 2002.

2. BD94. J. R. Burch and D. L. Dill. Automatic verification of pipelined microprocessors control. In CAV 94, volume 818, pages 68-80. Springer-Verlag, 1994.

3. BerOl. Christoph Berg. Formal verification of an IEEE floating point adder.

4. Master's thesis, Saarland University, Saarbrücken, Germany, May 2001.

5. Bey05. Sven Beyer. Putting it all together—Formal Verification of the VAMP. PhD thesis, Saarland University, Saarbrücken, Germany, 2005.

6. BHK94. B. Brock, W. A. Hunt, and M. Kaufmann. The FM9001 microprocessor proof. Technical Report 86, Computational Logic Inc., 1994.

7. BJ01. Christoph Berg and Christian Jacobi. Formal verification of the VAMP floating point unit. In CHARME 2001, volume 2144 of LNCS, pages 325-339. Springer, 2001.

8. BJK01. Christoph Berg, Christian Jacobi, and Daniel Kröning. Formal verification of a basic circuits library. In Proc. 19th IASTED International Conference on Applied Informatics, Innsbruck (AF2001), pages 252-255. ACTA Press, 2001.

9. Bog05. Sebastian Bogan. Formal Verification of a Simple Operating System (Draft). PhD thesis, Saarland University, Saarbrücken, Germany, 2005.

10. DHP05. I. Dalinger, M. Hillebrand, and W. Paul. On the verification of memory management mechanisms. In D. Borrione and W. Paul, editors, CHARME 2005, LNCS. Springer, 2005.

11. GHLP05. M. Gargano, M. Hillebrand, D. Leinenbach, and W. Paul. On the correctness of operating system kernels. In J. Hurd and T. Melham, editors, TPHOLs 2005 (to appear), LNCS. Springer, 2005.

12. Hil05. Mark Hillebrand. Address Spaces and Virtual Memory: Specification, Implementation, and Correctnesss. PhD thesis, Saarland University, Saarbrücken, Germany, 2005.

13. HIP05. Mark Hillebrand, Thomas In der Rieden, and Wolfgang Paul.

14. Dealing with I/O devices in the context of pervasive system verification. In I CCD '05. IEEE Computer Society, 2005. To appear.

15. HP96a. J. L. Hennessy and D. A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann, San Mateo, CA, second edition, 1996.

16. HP96b. John L. Hennessy and David A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann Publishers, INC., San Mateo, CA, 2nd edition, 1996.

17. HS99. W. A. Hunt and J. Sawada,. Verifying the FM9801 microarchitecture. In IEEE Micro, pages 47-55, 1999.

18. HSG99. Ravi Hosabettu, Mandayam Srivas, and Ganesh Gopalakrishnan.

19. Proof of correctness of a processor with reorder buffer using the completion functions approach. In Computer-Aided Verification, CAV '99, volume 1633, pages 47-59. Springer-Verlag, 1999.

20. E85. Institute of Electrical and Electronics Engineers. ANSI/IEEE standard 75^-1985, IEEE Standard for Binary Floating-Point Arithmetic, 1985.

21. Jac02a. Christian Jacobi. Formal Verification of a fully IEEE-compliant Floating-Point Unit. PhD thesis, Saarland University, Saarbrücken, Germany, 2002.

22. JK00. Christian Jacobi and Daniel Kröning. Proving the correctness of a complete microprocessor. In Proc. of the 30. Jahrestagung der Gesellschaft four Informatik. Springer, 2000.

23. JM98. Bruce Jacob and Trevor Mudge. Virtual memory in contemporary microprocessors. IEEE Micro, 18(4):60—75, 1998.

24. JWPB05. C. Jacobi, K. Weber, V. Paruthi, and J. Baumgartner. Automatic Formal Verification of Fused-Multiply-Add FPUs. In DATE, pages 1298-1303, 2005.

25. McM98. K. McMillan. Verification of an implementation of Tomasulo's algorithm by compositional model checking. In CA V 98, volume 1427. Springer, June 1998.

26. MP00. Silvia M. Müller and Wolfgang J. Paul. Computer Architecture: Complexity and Correctness. Springer, 2000.

27. MS05. Panagiotis Manolios and Sudarshan K. Srinivasan. A parameterized benchmark suite of hard pipelined-machine-verification problems. In CHARME 2005, volume 3725 of LNCS, pages 363-366. Springer, 2005.

28. OSR92. S. Owre, N. Shankar, and J. M. Rushby. PVS: A prototype verification system. In CADE 11, volume 607 of LNAI, pages 748752. Springer, 1992.

29. Pet04. Elena Petrova. Formal Verification of Compilers on the Source Code Level (Draft). PhD thesis, Saarland University, Saarbrücken, Germany, 2004.

30. SH98. J. Sawada and W. A. Hunt. Processor verification with precise exceptions and speculative execution. In CAV 98, volume 1427 of LNCS. Springer, 1998.

31. SP88. James E. Smith and Andrew R. Pleszkun. Implementing precise interrupts in pipelined processors. In IEEE Transactions on Computers, volume C-37, pages 562-573. 1988.

32. Tom67. R. M. Tomasulo. An efficient algorithm for exploiting multiple arithmetic units. In IBM Journal of Research & Development, volume 11 (1), pages 25-33. IBM, 1967.

33. Tve05a. Sergey Tverdyshev. Combination of Isabelle/HOL with automatic tools. In 5th International Workshop on Frontiers of Combining Systems (FroCoS)(to appear), Lecture Notes in Artificial Intelligence. Springer, 2005.

34. Tve05b. Sergey Tverdyshev. Formal Verification of the VAMP processor by using automated methods (Draft). PhD thesis, Saarland University, Saarbrücken, Germany, 2005.

35. VB99. M. Velev and R. Bryant. Superscalar processor verification using efficient reductions of the logic of equality with uninterpreted functions to propositional logic. In L. Pierre and T. Kropf, editors, CHARME 1999, LNCS. Springer, 1999.

36. VB00. Miroslav N. Velev and Randal E. Bryant. Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction. In DAC. ACM, 2000.

37. Ver03. The Verisoft Project, http://www.verisoft.de/, 2003.