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

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

image


Как это было

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


От Rust к Embedded

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

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

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

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


А где же RISC-V?

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

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


  • 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


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

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

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

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

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


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

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

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


Почему F#

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

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

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

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

Чем сейчас для меня стал F#? Достаточно гибким языком, с очень удобными IDE (Rider, Visual Studio). Вполне развитыми типами (хотя конечно до 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. Если у вас не установлено, то к примеру, под Ubuntu 16.04 необходимо выполнить такой набор команд: 

$ 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

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

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


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

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

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

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


© Habrahabr.ru