Como cheguei à especificação formal de um processador RISC-V em F #

Nas lânguidas noites de inverno, quando o sol passava preguiçosamente pelo véu dos dias, encontrei forças para enfrentar a realização de um sonho de longa data: descobrir como os processadores estão dispostos. Esse sonho me levou a escrever uma especificação formal de processador RISC-V. Projeto Github


imagem


Como foi


Eu tinha esse desejo há muito tempo, quando há 20 anos comecei a participar dos meus primeiros projetos. Na maioria das vezes, tratavam-se de pesquisa científica, modelagem matemática no âmbito de trabalhos e artigos científicos. Estes foram os dias de Pascal e Delfos. No entanto, mesmo assim, Haskell e a programação funcional atraíram meu interesse. O tempo passou, os idiomas dos projetos e tecnologias em que eu estava envolvido mudaram. Mas desde então o interesse em linguagens de programação funcional tem sido um fio comum, e eles se tornaram: Haskell, Idris, Agda. Recentemente, no entanto, meus projetos estiveram em Rust. Uma imersão mais profunda no Rust me levou a estudar dispositivos incorporados.


Da ferrugem ao incorporado


Os recursos do Rust são tão amplos e a comunidade é tão ativa que o desenvolvimento incorporado começou a oferecer suporte a uma ampla gama de dispositivos. E este foi o meu primeiro passo para um entendimento de nível inferior dos processadores.


Minha primeira placa foi: STM32F407VET6 . Foi uma imersão no mundo dos microcontroladores, da qual naquela época eu estava muito longe, e compreendi o suficiente sobre como o trabalho era feito em um nível baixo.


Gradualmente, as placas esp32 , ATmega328 (representadas pela placa ucraniana da ONU ) foram adicionadas aqui. A imersão no stm32 acabou sendo bastante dolorosa - as informações são abundantes e geralmente não são as que eu preciso. E aconteceu que desenvolver, por exemplo, no Assembler é uma tarefa bastante rotineira e ingrata, com seu subconjunto de mais de 1000 instruções. No entanto, Rust lidou com isso alegremente, embora às vezes houvesse dificuldades com a integração de placas chinesas específicas.


A arquitetura do AVR acabou sendo notavelmente mais simples e mais transparente. Os manuais abundantes me deram compreensão suficiente de como trabalhar com um conjunto de instruções tão limitado e, no entanto, consegui criar soluções muito interessantes. No entanto, o caminho do Arduino não me agradou nada, mas escrever em Asm / C / Rust acabou sendo muito mais interessante.


Onde está o RISC-V?


E, nesse momento, surge uma pergunta lógica - onde está a CPU RISC-V ?
É a natureza minimalista do AVR e sua documentação suficiente que me trouxe de volta ao meu sonho anterior para descobrir como o processador funciona. Nessa época, eu tinha uma placa FPGA e as primeiras implementações para ela na forma de interação com dispositivos VGA, saída gráfica, interação com periféricos.


Os livros foram meus guias para a arquitetura do processador:


  • John L. Hennessy e David A. Patterson - Arquitetura de Computadores: Uma Abordagem Quantitativa (A Série Morgan Kaufmann em Arquitetura e Design de Computadores)
  • John L. Hennessy e David A. Patterson - Organização e Design de Computadores. A interface de hardware / software: RISC-V Edition
  • David M. Harris e Sarah L. Harris - circuitos digitais e arquitetura de computadores
  • O manual do conjunto de instruções do RISC-V

Por que isso é necessário?


Parece - tudo já foi escrito e implementado por um longo tempo.



várias implementações em HDL e linguagens de programação. A propósito, uma implementação bastante interessante do RISC-V on Rust .


No entanto, o que poderia ser mais interessante do que descobrir você mesmo e criar o seu próprio. Sua bicicleta ? Ou contribuir para a construção de bicicletas ? Além do profundo interesse pessoal, tive uma ideia - como tentar popularizar, interessar. E encontre seu formulário, sua abordagem. E isso significa apresentar a documentação bastante chata do RISC-V ISA na forma de uma especificação oficial de uma forma diferente. E parece-me que o caminho da formalização nesse sentido é bastante interessante.


O que quero dizer com formalização? Um conceito bastante amplo. Representação de um conjunto de dados específico de forma formal. Neste caso, através de uma descrição de estruturas e uma descrição funcional. E, nesse sentido, as linguagens de programação funcionais têm seu próprio charme. Além disso, a tarefa é que uma pessoa que não esteja muito imersa em programação possa ler o código como uma especificação, se possível entender minimamente as especificidades da linguagem na qual está descrito.
Uma abordagem declarativa, por assim dizer. Há uma declaração, mas como exatamente funciona não é mais essencial. O principal é a legibilidade, a visibilidade e, é claro, a correção. Correspondência de declarações formais com o significado nelas incorporado.
imagem
Total - estou realmente curioso para passar meu interesse para os outros. Há uma certa ilusão de que o interesse é a força motriz das ações. Através do qual a individualidade se torna e se manifesta. E isso faz parte da auto-realização, a personificação da criatividade.
Ambicioso e um pouco de letras. O que vem depois?


Implementações existentes


Eles existem e atualmente estão sendo agregados pelo projeto: Verificação formal do RISC-V .
Lista de especificações formais (incluindo meu trabalho): https://github.com/SymbioticEDA/riscv-formal/blob/master/docs/references.md


Como você pode ver - na maior parte, são formalizações na linguagem Haskell. Este foi o ponto de partida na escolha de uma linguagem funcional diferente. E minha escolha caiu em F # .


Por que F#


Acontece que eu conheço o F # há muito tempo, mas, de alguma forma, na agitação da vida cotidiana, não tive oportunidade de me conhecer melhor. Outro fator foi a plataforma .NET . Tendo em conta que estou no Linux, durante muito tempo não fiquei satisfeito com o IDE, e o mono parecia bruto o suficiente. E retornar ao Windows apenas pelo MS Visual Studio é uma ideia bastante duvidosa.


No entanto, o tempo não pára e as estrelas no céu não têm pressa de mudar. Mas, a essa altura, o Jetbrains Rider havia evoluído para uma ferramenta completa e conveniente, e o .NET Core para Linux não traz dor de relance.


A questão era - qual linguagem funcional escolher. O fato de que deveria ser apenas uma linguagem funcional - de uma forma um tanto patética, argumentei acima.
Haskell, Idris, Agda ? F# - Não estou familiarizado com ele. Uma ótima ocasião para aprender novas cores do mundo das linguagens funcionais.


Sim, o F# não F# puramente funcional. Mas o que impede a adesão à " pureza "? E então aconteceu - que a documentação do F # é bastante detalhada e completa. Legível, e eu diria até interessante.


O que é F# para mim agora? Uma linguagem bastante flexível, com IDEs muito convenientes (Rider, Visual Studio). Tipos completamente desenvolvidos (embora, Idris claro, Idris muito longe). E, no geral, muito doce em termos de legibilidade. No entanto, como se viu, sua funcional " não limpeza " - pode levar o código a uma forma completamente insana, tanto em termos de legibilidade quanto de lógica. A análise de pacotes no Nuget demonstra isso.


Outro recurso interessante e misterioso para mim foi a descoberta de que ninguém estava interessado em escrever a formalização do RISC-V ISA em F # antes (oficialmente ou em uma forma pesquisável). E isso significa que tenho a chance de introduzir um novo fluxo nessa comunidade, idioma e " ecossistema ".


As armadilhas que encontrei


A parte mais difícil foi a implementação do fluxo de execução. Aconteceu com frequência que não estava totalmente claro como a instrução deveria funcionar. Infelizmente, um amigo de confiança que poderia ser chamado às três da manhã e perguntou com uma voz empolgada e aspirada: "Sabe, a instrução BLTU provavelmente significa significar de maneira diferente ..." - Eu não. Nesse sentido, ter camaradas qualificados que ajudarão com uma palavra gentil e aconselhamento qualificado apropriado é muito bem-vindo.


Quais foram as dificuldades e armadilhas. Vou tentar a tese:


  • ELF - uma tarefa curiosa era descobrir como trabalhar com ele, ler seções, instruções. Muito provavelmente, essa história dentro da estrutura do projeto atual não está concluída.
  • instruções não assinadas periodicamente levavam a erros que eu detectava durante o teste de unidade
  • a implementação do trabalho com a memória necessária para pensar em algoritmos de composição de bytes bonitos e legíveis.
  • não havia um pacote adequado para trabalhar com bits em int32, int64 . Demorou tempo para escrever meu pacote e testá-lo.
    Aqui, quero observar que trabalhar com bits em F # é muito mais conveniente do que em Haskell com seus Data.Bits
  • suporte adequado para bits de registro, com a capacidade de suportar x32 e x64 ao mesmo tempo. A desatenção me levou a usar o int64 em alguns lugares. Os testes de unidade me ajudaram a identificar isso. Mas demorou um pouco.
  • Não encontrei um pacote CLI F # simples, conciso e pessoalmente conveniente para mim. Um efeito colateral foi escrever uma versão minimalista em um estilo funcional.
  • No momento, ainda é um mistério como implementar corretamente as Instruções do sistema: CERCA, ECALL, BREAK
  • longe de todo o conjunto de extensões (extensões ISA) da lista: [A, M, C, F, D] atualmente óbvias. Em particular, a implementação de [F,D] não [F,D] por meio soft float .
  • no momento, não há um entendimento claro das Instruções Privilegiadas, User Mod, funcionam com periféricos - infelizmente. E este é o caminho da pesquisa, tentativa e erro.
  • Não há faixa preta para escrever programas Assembler no RISC-V. Talvez esteja longe de ser uma necessidade, dado o número de idiomas que já foram portados para escrita no RISC-V.
  • o fator tempo também foi significativo - é bastante pequeno no turbilhão do trabalho básico, nas necessidades diárias e no oceano da vida ao redor. E há muito trabalho, e a maior parte não é tanto em " codificação " - escrever o próprio código, mas em aprender, dominar os materiais.

Como funciona e quais recursos


Agora talvez a parte mais técnica . Quais são os recursos no momento:


  • rv32i conjunto de instruções rv32i
  • a capacidade de executar o programa como um simulador RISC-V - a execução de arquivos ELF.
  • suporte à linha de comando (CLI) - seleção da arquitetura executável, conjunto de instruções, arquivos ELF executáveis, modo de registro em log, ajuda na linha de comando.
  • a capacidade de exibir o log de instruções executáveis, perto da exibição objdump ao desmontar.
  • a capacidade de executar testes que abrangem todo o conjunto de instruções implementado.

O programa é dividido em etapas e ciclos:


  • ler linha de comando
  • ler instruções de um arquivo ELF
  • lendo uma instrução específica de acordo com o contador atual do PC (contador de programas)
  • instruções de decodificação
  • execução de instruções
  • no caso de situações imprevistas, armadilhas são configuradas, permitindo concluir o processo de execução, sinalizando um problema e fornecendo os dados necessários
  • se o programa não estiver em um loop infinito - exiba o estado dos registros e finalize o programa de simulação

O que está incluído nos planos:


  • Base 64i padrão (quase completa)
  • Extensão padrão M (número inteiro multiplicar / dividir)
  • Extensão padrão A (operações de memória atômica)
  • Extensão padrão C (instruções compactadas de 16 bits)
  • Extensão padrão F (ponto flutuante de precisão única)
  • Extensão padrão D (ponto flutuante de dupla precisão * Nível de privilégio M (Máquina)
  • Nível de privilégio U (usuário)
  • Privilégio Nível S (Supervisor)
  • Esquemas de memória virtual SV32, SV39 e SV48
  • programas hospedeiros
  • GPIO - trabalhe com periféricos

Como executar


Para executar o programa, você deve ter o .NET Core . Se você não o instalou, por exemplo, no Ubuntu 16.04 é necessário executar o seguinte conjunto de comandos:


 $ 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 

Para verificar se algo na vida mudou, execute:


 $ dotnet --version 

E a vida deve brilhar com novas cores!


Agora tente correr. Para fazer isso, compre seu chá ou café favorito, chocolate com pãezinhos, ative sua música favorita e siga este conjunto de comandos:


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

e seu console deve piscar de brincadeira para você com uma mensagem de ajuda.
O lançamento é:


 $ dotnet run 

Num tom estrito, ele dirá que são necessários parâmetros. Portanto, execute:


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

Esse é o mesmo momento embaraçoso em que ainda precisamos de um programa pronto para execução para o RISC-V. E há algo para eu ajudá-lo. No entanto, você precisará da cadeia de ferramentas GNU para RISC-V . Deixe que seja instalado o dever de casa - a descrição do repositório descreve em detalhes suficientes como fazer isso.


Em seguida, para obter o arquivo ELF de teste cobiçado, executamos as seguintes ações:


 $ cd Tests/asm/ $ make build32 

Se você possui uma cadeia de ferramentas RISC-V , tudo deve ocorrer sem problemas. E os arquivos devem aparecer no diretório:


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

e agora com ousadia, sem olhar para trás, tentamos o comando:


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

É importante observar que o Tests/asm não Tests/asm um programa de teste, mas seu principal objetivo são as instruções de teste e seus códigos para escrever testes. Portanto, se você gosta de algo maior e mais heróico, mudar o mundo à sua vontade é encontrar um arquivo ELF de 32 bits executável independentemente, que suporte apenas instruções rv32i .


No entanto, o conjunto de instruções e extensões será reabastecido, ganhando impulso e ganhando peso.


Resumo e links


Acabou sendo uma narração um pouco patética, aromatizada pela história pessoal. Algumas vezes técnicas, outras subjetivas. No entanto entusiasmado e com um toque de entusiasmo.


Da minha parte, estou interessado em ouvir de você: críticas, impressões, boas palavras de despedida. E para os mais ousados ​​- ajude no apoio ao projeto.


Você está interessado em um formato narrativo e gostaria de continuar?


Source: https://habr.com/ru/post/pt473714/


All Articles