Хабрахабр

Как я пришел к формальной спецификации RISC-V процессора на F#

Эта мечта привела меня к написанию формально спецификации RISC-V процессора. Томными зимними вечерами, когда солнце лениво пробегало сквозь пелену дней — я нашел в себе силы заняться реализацией давней мечты: разобраться как же устроены процессоры. Проект на Github

image

Как это было

По большей части это были научные исследования, математическое моделирование в рамках курсовых работ и научных статей. Подобное желание у меня появилось достаточно давно, когда 20 лет назад я стал заниматься первыми своими проектами. Однако уже тогда мой интерес привлек Haskell и функциональное программирование. Это были времена Pascal и Delphi. Но с тех пор красной нитью проходил интерес к функциональным языкам программирования, и ими стали: Haskell, Idris, Agda. Прошло время, менялись языки проектов и технологии в которые я был вовлечен. Более глубокое погружение в Rust меня привело к изучению Embedded устройств. Однако в последнее время мои проекты были на языке Rust.

От Rust к Embedded

И это был мой первый шаг в более низкоуровневое понимание процессоров. Возможности Rust настолько широки, а community настолько активно, что Embedded разработка стала поддерживать широкий спектр устройств.

Это было погружение в мир микроконтроллеров, от которого я на тот момент был очень далек, и достаточно приблизительно понимал как происходит работа на низком уровне. Первой моей платой стало: STM32F407VET6.

Погружение в stm32 оказалось достаточно болезненным — информация достаточно обильная и часто не та, которая мне нужна. Постепенно сюда добавились платы esp32, ATmega328 (в лице платы Ukraino UNO). Однако Rust с этим справлялся бодро, хотя порой возникали трудности с интеграцией для конкретных китайских плат. И оказалось, что разработка, к примеру, на Assembler — достаточно рутинная и неблагодарная задача, с их подмножеством более 1000 инструкций.

Обильные мануалы мне дали достаточное понимание как работать с таким достаточно ограниченным набором инструкций, и тем не менее иметь возможность создавать очень интересные решения. Архитектура AVR оказалась заметно проще и прозрачнее. Тем не менее путь Arduino меня совсем не радовал, но вот написание на Asm/C/Rust оказалось куда увлекательнее.

А где же RISC-V?

К этому времени у меня появилась FPGA плата и первые реализации для нее в виде взаимодействия с VGA устройствами, вывода графики, взаимодействия с периферией. И в этот момент возникает логичный вопрос — а где же RISC-V CPU?
Именно минималистичность AVR и достаточное его документирование, меня вернули к прежней мечте разобраться как же работает процессор.

Моими проводниками в архитектуру процессоров стали книги:

  • John L. Hennessy and David A. Patterson — Computer Architecture: A Quantitative Approach (The Morgan Kaufmann Series in Computer Architecture and Design)
  • John L. Hennessy and David A. Patterson — Computer Organization and Design. The Hardware/Software Interface: RISC-V Edition
  • Дэвид М. Хэррис и Сара Л. Хэррис — Цифровая схемотехника и архитектура компьютера
  • The RISC-V Instruction Set Manual

Зачем это нужно

Казалось бы — уже все давно написано и реализовано.

Кстати достаточно интересная реализация RISC-V на Rust. разнообразные реализации на HDL, и языках программирония.

Свой велосипед? Однако что может быть интереснее, чем разобраться самому, и создать свое. Кроме личного глубокого интереса у меня возникла идея — а как попробовать популяризировать, заинтересовать. Или внести свой вклад в велосипедостроение? А это значит представить достаточно скучную документацию по RISC-V ISA в виде официальной спецификации в ином виде. И найти свою форму, свой подход. И мне кажется путь формализации в этом смысле достаточно интересен.

Достаточно обширное понятие. Что я понимаю под формализацией? В данном случае через описание структур и функционального описания. Представление определенного набора данных в формальном виде. Также задача в том — чтобы человек который не сильно погружен в программирование мог прочитать код как спецификацию, по-возможности минимально вникая в специфику языка, на котором это описано.
Декларативный подход, так сказать. И в этом смысле функциональные языки программирования обладают своим очарованием. Главное читабельность, наглядность, и конечно же корректность. Есть высказывание, а как именно это работает — это уже не существенно. Есть некая иллюзия того, что интерес — движущая сила к поступкам. Соответствие формальных высказываний вкладываемому в них смыслу.
image
Итого — мне действительно любопытно передать свой интерес другим. И в этом есть часть самореализации, воплощение творческого начала.
Амбициозно и немного лирики. Через что становится и проявляется индивидуальность. Что же дальше?

Существующие реализации

Они есть и на данный момент их агрегирует проект: RISC-V Formal Verification.
Список формальных спецификаций (включая мою работу): https://github.com/SymbioticEDA/riscv-formal/blob/master/docs/references.md

Это стало отправной идеей в выборе другого функционального языка. Как видно — по большей части это формализации на языке Haskell. И мой выбор пал на F#.

Почему F#

Еще одним фактором была . Так случилось, что про F# мне известно давно, но все как-то в суете повседневности не имел возможности познакомиться ближе. Беря во внимание что я под Linux-ом, долгое время меня не устраивали IDE, и mono выглядело достаточно сырым. NET платформа. А возвращение в Windows только ради MS Visual Studio — достаточно сомнительная идея.

Но к этому времени Jetbrains Rider — развился до полноценного и удобного инструмента, а . Однако время не стоит на месте, а звезды на небе не спешат меняться. NET Core для Linux не приносит боль при одном взгляде на него.

То что это должен быть именно функциональный язык — в несколько патетическом виде я аргументировал выше.
Haskell, Idris, Agda? Стал вопрос — какой функциональный язык выбрать. Отличный повод узнать новые краски мира функциональных языков. F# — с ним я не знаком.

Но что мешает придерживаться "чистоты"? Да F# не чисто-функциональный. Читабельная, и я бы даже сказал интересная. И тут оказалось — что F# документация достаточно подробная и целостная.

Достаточно гибким языком, с очень удобными IDE (Rider, Visual Studio). Чем сейчас для меня стал F#? И в целом достаточно милым с точки зрения читабельности. Вполне развитыми типами (хотя конечно до Idris очень далеко). Анализ пакетов в Nugget это наглядно показывает. Однако как оказалось его функциональная "не чистота" — может приводить код к совершенно невменяемому виду как с точки зрения читабельности, так и логики.

А это значит, что у меня есть шанс внести новую струю в это сообщество, язык, "экосистему". Еще одной интересной и загадочной особенностью для меня стало открытие, что написать формализацию RISC-V ISA на F# ранее никого не интересовало (официально или в доступном для поиска виде).

Подводные камни, с которыми я столкнулся

Часто оказывалось, что не до конца понятно как инструкция должна работать. Самой сложной частью оказалось реализация Execution flow. В этом смысле иметь квалифицированных товарищей, которые добрым словом и уместным квалифицированным советом помогут — очень желанно. К сожалению надежного товарища, которому можно было бы позвонить в 3 часа ночи и взволнованным голосом с придыханием спросить: "А знаешь, BLTU инструкция наверное по-другому signextend-ится..." — у меня нет.

Попробую тезисно: Какие были трудности и подводные камни.

  • ELF — любопытной задачей стало разобраться как с ним работать, читать секции, инструкции. Скорее всего эта история в рамках текущего проекта не закончена.
  • unsigned инструкции периодически меня приводили к ошибкам, которые я выявлял в процессе unit-тестирования
  • реализация работы с памятью потребовала подумать над красивыми и читабельными алгоритмами компановки байтов.
  • годного пакета для работы с битами под int32, int64 не оказалось. Потребовалось время на написание своего пакета и на его тестирование.
    Здесь хочу отметить, что работа с битами в F# таки в разы удобнее чем в Haskell с его Data.Bits
  • правильная поддержка битности регистров, с возможностью поддержки x32 и x64 одновременно. Невнимательность привела к тому, что я в некоторых местах использовал int64. Выявить это мне помогли unit-тесты. Но на это потребовалось время.
  • простого, лаконичного, удобного лично мне CLI F# пакета я не нашел. Побочным эффектом стало написание минималистичного варианта в функциональном стиле
  • на данный момент остается загадкой как правильно реализовать System Instructions: FENCE, ECALL, BREAK
  • далеко не весь набор расширений (ISA extensions) из списка: [A, M, C, F, D] на данный момент очевидны. В особенности реализация [F,D] не через soft float.
  • на данный момент ясного понимания Privileged Instructions, User Mod, работы с периферией — увы нет. И это путь исследований, проб и ошибок.
  • нет черного пояса по написанию Assembler программ под RISC-V. Возможно далеко не часто в этом будет потребность, учитывая сколько языков уже портировано для написания под RISC-V.
  • также существенным оказался фактор времени — его достаточно мало в водовороте основной работы, житейских потребностей и океана жизни вокруг. А работы достаточно много, и большая часть не столько в "кодировании" — написания самого кода, сколько в изучении, осваивания материалов.

Как это работает и какие возможности

Какие возможности на данный момент: Теперь пожалуй наиболее техническая часть.

  • выполнение набора инструкций rv32i
  • возможность выполнения программы в качестве RISC-V симулятора — выполнения ELF-файлов.
  • поддержка командной строки (CLI) — выбор выполняемой архитектуры, набора инструкций, исполняемых ELF-файлов, режима логирования, справки по командной строке.
  • возможность вывода лога выполняемых инструкций, приближенного к objdump виду при дизассемблировании.
  • возможность запуска тестов покрывающих весь реализованный набор инструкций.

Работа программы разделена на такие этапы и циклы:

  • чтение командной строки
  • чтение инструкций из ELF-файла
  • чтение конкретной инструкции согласно текущему PC (Program Counter) — счетчику
  • декодирование инструкции
  • выполнение инструкции
  • при наличии непредвиденных ситуаций расставлены ловушки (Trap), позволяющие завершить процесс выполнения, сигнализирующие о проблеме, и предоставляющие необходимые данные
  • в случае если программа не в бесконечном цикле — вывод состояния регистров и завершение программы симулирования

Что входит в планы:

  • Standard base 64i (почти завершено)
  • Standard extension M (integer multiply/divide)
  • Standard extension A (atomic memory ops)
  • Standard extension C (Compressed 16-bit instructions)
  • Standard extension F (Single-precision floating point)
  • Standard extension D (Double-precision floating point* Privilege Level M (Machine)
  • Privilege Level U (User)
  • Privilege Level S (Supervisor)
  • Virtual Memory schemes SV32, SV39 and SV48
  • host программы
  • GPIO — работа с периферией

Как запустить

NET Core. Для того чтобы запустить программу необходимо наличие . 04 необходимо выполнить такой набор команд: Если у вас не установлено, то к примеру, под Ubuntu 16.

$ wget -q https://packages.microsoft.com/config/ubuntu/16.04/packages-microsoft-prod.deb -O packages-microsoft-prod.deb
$ sudo dpkg -i packages-microsoft-prod.deb
$ sudo apt-get update
$ sudo apt-get install apt-transport-https
$ sudo apt-get update
$ sudo apt-get install dotnet-sdk-3.0

Чтобы проверить, что что-то в жизни изменилось — запустите:

$ dotnet --version

И жизнь должна заиграть новыми красками!

Для этого запаситесь любимым чаем или кофе, шоколадкой с плюшками, включите любимую музыку и выполните такой набор команд: Теперь попробуем запустить.

$ cd some/my/dev/dir
$ git clone https://github.com/mrLSD/riscv-fs
$ cd riscv-fs
$ dotnet build
$ dotnet run -- --help

и ваша консоль должна игриво подмигнуть вам справочным сообщением.
Запуск же:

$ dotnet run

Поэтому запускаем: Строгим тоном скажет — что нужны параметры.

$ dotnet run -- -A rv32i -v myapp.elf

И тут есть мне чем вам помочь. Это тот самый неловкий момент, когда оказывается, что все-таки нам нужна уже готовая ready for execution программа под RISC-V. Его установка пусть будет домашним заданием — в описании к репозиторию достаточно детально описано как это делать. Однако вам понадобится GNU toolchain for RISC-V.

Далее, для получения заветного тестового ELF-файла, выполняем такие действия:

$ cd Tests/asm/
$ make build32

И файлики должны красоваться в директории: если у вас RISC-V toolchain есть в наличии то все должно пройти гладко.

$ ls Tests/asm/build/
add32 alu32 alui32 br32 j32 mem32 sys32 ui32

и теперь смело, без оглядки пробуем команду:

$ dotnet run -- -A rv32i -v Tests/asm/build/ui32

Поэтому если вам что-то по душе более масштабное и героическое, то в вашей воле меняя мир — найти самостоятельно исполняемый 32-битный ELF файл с поддержкой только rv32i инструкций. Важно отметить, что Tests/asm не является тестовыми программами, но их основная цель — это тестовые инструкции и их коды для написания тестов.

Однако набор инструкций и расширений будет пополняться, набирать обороты и приобретать вес.

Резюме и ссылки

Временами техническое, порой субъективное. Получилось немного патетическое, приправленное личной историей повествование. Однако воодушевленное и с легким налетом энтузиазма.

А для самых смелых — помощь в поддержании проекта. С моей же стороны мне интересно от вас услышать: отзывы, впечатления, добрые напутствия.

Интересен ли вам такой формат повествования и хотели бы вы продолжений?

Теги
Показать больше

Похожие статьи

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *

Кнопка «Наверх»
Закрыть