Bagaimana saya sampai pada spesifikasi formal prosesor RISC-V di F #

Pada malam musim dingin yang tenang, ketika matahari dengan malas melewati tabir hari, saya menemukan kekuatan untuk mengatasi realisasi dari mimpi yang telah lama dipegang: untuk mencari tahu bagaimana prosesor diatur. Mimpi ini membuat saya menulis spesifikasi prosesor RISC-V formal. Proyek Github


gambar


Bagaimana itu?


Saya memiliki keinginan yang sangat lama, ketika 20 tahun yang lalu saya mulai terlibat dalam proyek pertama saya. Sebagian besar, ini adalah penelitian ilmiah, pemodelan matematika dalam kerangka makalah dan artikel ilmiah. Ini adalah zaman Pascal dan Delphi. Namun, bahkan kemudian, Haskell dan pemrograman fungsional menarik minat saya. Waktu berlalu, bahasa proyek dan teknologi tempat saya terlibat berubah. Tetapi sejak itu minat dalam bahasa pemrograman fungsional telah menjadi benang merah, dan mereka telah menjadi: Haskell, Idris, Agda. Namun, baru-baru ini, proyek saya ada di Rust. Perendaman yang lebih dalam di Rust membuat saya mempelajari perangkat Embedded.


Dari Karat ke Tertanam


Kemampuan Rust sangat luas, dan komunitasnya sangat aktif sehingga pengembangan Embedded telah mulai mendukung berbagai perangkat. Dan ini adalah langkah pertama saya ke tingkat pemahaman prosesor yang lebih rendah.


Papan pertama saya adalah: STM32F407VET6 . Itu adalah perendaman dalam dunia mikrokontroler, yang saat itu saya sangat jauh, dan cukup memahami bagaimana pekerjaan itu dilakukan pada tingkat rendah.


Secara bertahap, esp32 , papan ATmega328 (diwakili oleh papan Ukraino UNO ) ditambahkan di sini. Perendaman dalam FM32 ternyata cukup menyakitkan - informasinya berlimpah dan seringkali bukan yang saya butuhkan. Dan ternyata mengembangkan, misalnya, di Assembler adalah tugas yang agak rutin dan tidak berterima kasih, dengan subset mereka lebih dari 1000 instruksi. Namun, Rust mengatasi hal ini dengan riang, meskipun kadang-kadang ada kesulitan dengan integrasi untuk papan Cina tertentu.


Arsitektur AVR ternyata lebih sederhana dan lebih transparan. Buku pedoman yang melimpah memberi saya pemahaman yang cukup tentang cara bekerja dengan seperangkat instruksi yang cukup terbatas, dan bagaimanapun dapat membuat solusi yang sangat menarik. Meskipun demikian, jalur Arduino tidak menyenangkan saya sama sekali, tetapi menulis dalam Asm / C / Rust ternyata jauh lebih menarik.


Di mana RISC-V?


Dan pada saat itu muncul pertanyaan logis - di mana CPU RISC-V ?
Ini adalah sifat minimalis AVR dan dokumentasinya yang memadai yang membawa saya kembali ke mimpi saya sebelumnya untuk mencari tahu bagaimana prosesor bekerja. Pada saat ini, saya memiliki papan FPGA dan implementasi pertama untuk itu dalam bentuk interaksi dengan perangkat VGA, output grafis, interaksi dengan periferal.


Buku adalah panduan saya untuk arsitektur prosesor:


  • John L. Hennessy dan David A. Patterson - Arsitektur Komputer: Pendekatan Kuantitatif (Seri Morgan Kaufmann dalam Arsitektur dan Desain Komputer)
  • John L. Hennessy dan David A. Patterson - Organisasi dan Desain Komputer. Antarmuka Perangkat Keras / Perangkat Lunak: Edisi RISC-V
  • David M. Harris dan Sarah L. Harris - Sirkuit digital dan arsitektur komputer
  • Manual Set Instruksi RISC-V

Mengapa itu perlu?


Tampaknya - semuanya sudah ditulis dan diimplementasikan untuk waktu yang lama.



berbagai implementasi dalam HDL, dan bahasa pemrograman. Omong-omong, implementasi RISC-V pada Rust cukup menarik.


Namun, apa yang bisa lebih menarik daripada mencari tahu sendiri dan membuatnya sendiri. Sepeda Anda? Atau berkontribusi pada pembangunan sepeda ? Selain minat pribadi yang mendalam, saya punya ide - bagaimana mencoba mempopulerkan, menarik. Dan temukan formulir Anda, pendekatan Anda. Dan itu berarti menghadirkan dokumentasi RISC-V ISA yang agak membosankan dalam bentuk spesifikasi resmi dalam bentuk yang berbeda. Dan menurut saya jalan formalisasi dalam pengertian ini cukup menarik.


Apa yang saya maksud dengan formalisasi? Konsep yang cukup luas. Representasi dari set data spesifik dalam bentuk formal. Dalam hal ini, melalui deskripsi struktur dan deskripsi fungsional. Dan dalam pengertian ini, bahasa pemrograman fungsional memiliki daya tarik tersendiri. Juga, tugasnya adalah bahwa seseorang yang tidak terlalu tenggelam dalam pemrograman dapat membaca kode sebagai spesifikasi, jika mungkin minimal memahami secara spesifik bahasa yang dijelaskan.
Pendekatan deklaratif, bisa dikatakan. Ada pernyataan, tetapi bagaimana tepatnya itu bekerja tidak lagi penting. Yang utama adalah keterbacaan, visibilitas, dan tentu saja kebenaran. Korespondensi pernyataan formal dengan makna yang tertanam di dalamnya.
gambar
Total - Saya benar-benar ingin menyampaikan minat saya kepada orang lain. Ada ilusi tertentu bahwa bunga adalah kekuatan pendorong untuk bertindak. Melalui mana individualitas menjadi dan memanifestasikan. Dan ini adalah bagian dari realisasi diri, perwujudan kreativitas.
Ambisius dan sedikit lirik. Apa selanjutnya


Implementasi yang Ada


Mereka ada dan saat ini sedang dikumpulkan oleh proyek: Verifikasi Formal RISC-V .
Daftar spesifikasi formal (termasuk pekerjaan saya): https://github.com/SymbioticEDA/riscv-formal/blob/master/docs/references.md


Seperti yang Anda lihat - sebagian besar ini adalah formalisasi dalam bahasa Haskell. Ini adalah titik awal dalam memilih bahasa fungsional yang berbeda. Dan pilihan saya jatuh pada F # .


Mengapa F#


Kebetulan saya sudah tahu tentang F # untuk waktu yang lama, tapi entah bagaimana dalam hiruk pikuk kehidupan sehari-hari saya tidak memiliki kesempatan untuk mengenal satu sama lain dengan lebih baik. Faktor lain adalah platform .NET . Mempertimbangkan bahwa saya berada di Linux, untuk waktu yang lama saya tidak senang dengan IDE, dan mono terlihat cukup mentah. Dan kembali ke Windows hanya demi MS Visual Studio adalah ide yang agak meragukan.


Namun, waktu tidak berhenti, dan bintang-bintang di langit tidak terburu-buru untuk berubah. Tetapi pada saat ini, Jetbrains Rider telah berevolusi menjadi alat yang lengkap dan nyaman, dan .NET Core untuk Linux tidak membawa rasa sakit sekilas melihatnya.


Pertanyaannya adalah - bahasa fungsional mana yang harus dipilih. Fakta bahwa itu seharusnya hanya bahasa fungsional - dalam bentuk yang agak menyedihkan, saya berpendapat di atas.
Haskell, Idris, Agda ? F# - Saya tidak terbiasa dengannya. Kesempatan yang bagus untuk mempelajari warna-warna baru dunia bahasa fungsional.


Ya, F# tidak sepenuhnya berfungsi. Tetapi apa yang mencegah untuk mematuhi " kemurnian "? Dan kemudian ternyata - bahwa dokumentasi F # cukup rinci dan lengkap. Dapat dibaca, dan saya bahkan akan mengatakan menarik.


Apa F# untuk saya sekarang? Bahasa yang cukup fleksibel, dengan IDE yang sangat nyaman (Rider, Visual Studio). Jenis yang sepenuhnya dikembangkan (walaupun tentu saja Idris sangat jauh). Dan secara keseluruhan cukup manis dalam hal keterbacaan. Namun, ternyata, " non-kemurnian " fungsionalnya - dapat membawa kode ke bentuk yang benar-benar gila, baik dari segi keterbacaan dan logika. Analisis paket di Nuget menunjukkan hal ini.


Fitur lain yang menarik dan misterius bagi saya adalah penemuan bahwa tidak ada yang tertarik untuk menulis formalisasi RISC-V ISA di F # sebelumnya (secara resmi atau dalam bentuk yang dapat dicari). Dan ini berarti saya memiliki kesempatan untuk memperkenalkan aliran baru ke komunitas, bahasa, dan “ ekosistem ” ini.


Perangkap yang saya temui


Bagian yang paling sulit adalah pelaksanaan aliran Eksekusi. Sering kali ternyata tidak sepenuhnya jelas bagaimana instruksi harus bekerja. Sayangnya, saya tidak bisa bertanya pada kawan yang bisa menelepon pada jam 3 pagi dengan suara penuh aspirasi: "Anda tahu, instruksi BLTU mungkin berbeda dalam signextend ..." Dalam hal ini, memiliki kawan-kawan yang memenuhi syarat yang akan membantu dengan kata-kata yang baik dan saran yang memenuhi syarat sangat disambut.


Apa kesulitan dan jebakannya. Saya akan mencoba tesis:


  • ELF - tugas yang aneh adalah untuk mengetahui bagaimana bekerja dengannya, membaca bagian, instruksi. Kemungkinan besar cerita ini dalam kerangka proyek saat ini belum selesai.
  • instruksi yang tidak ditandatangani secara berkala menyebabkan kesalahan yang saya deteksi selama pengujian unit
  • implementasi kerja dengan memori diperlukan untuk memikirkan algoritma komposisi byte yang indah dan mudah dibaca.
  • tidak ada paket yang cocok untuk bekerja dengan bit di bawah int32, int64 . Butuh waktu untuk menulis paket saya dan mengujinya.
    Di sini saya ingin mencatat bahwa bekerja dengan bit dalam F # jauh lebih nyaman daripada di Haskell dengan datanya. Bit
  • dukungan yang tepat untuk bit register, dengan kemampuan untuk mendukung x32 dan x64 bersamaan. Ketidakpedulian membuat saya menggunakan int64 di beberapa tempat. Tes unit membantu saya mengidentifikasi ini. Tapi butuh beberapa saat.
  • Saya tidak menemukan paket CLI F # sederhana, ringkas, mudah untuk saya pribadi. Efek sampingnya adalah menulis versi minimalis dengan gaya fungsional.
  • Saat ini, masih menjadi misteri bagaimana menerapkan Instruksi Sistem dengan benar: FENCE, ECALL, BREAK
  • jauh dari seluruh rangkaian ekstensi (ekstensi ISA) dari daftar: [A, M, C, F, D] saat ini jelas. Secara khusus, implementasi [F,D] tidak melalui soft float .
  • saat ini, tidak ada pemahaman yang jelas tentang Instruksi Privileged, Mod Pengguna, bekerja dengan periferal - sayangnya. Dan ini adalah cara penelitian, coba-coba.
  • Tidak ada sabuk hitam untuk menulis program Assembler di bawah RISC-V. Mungkin jauh dari sering ini akan menjadi kebutuhan, mengingat berapa banyak bahasa yang telah porting untuk ditulis di bawah RISC-V.
  • faktor waktu juga signifikan - cukup kecil dalam pusaran pekerjaan dasar, kebutuhan sehari-hari dan lautan kehidupan di sekitar. Dan ada banyak pekerjaan, dan sebagian besar tidak begitu banyak dalam " pengkodean " - menulis kode itu sendiri, tetapi dalam belajar, menguasai materi.

Cara kerjanya dan fitur apa


Sekarang mungkin bagian yang paling teknis . Apa saja fitur saat ini:


  • set instruksi rv32i
  • kemampuan untuk menjalankan program sebagai simulator RISC-V - eksekusi file ELF.
  • command line support (CLI) - pemilihan arsitektur yang dapat dieksekusi, sekumpulan instruksi, file ELF yang dapat dieksekusi, mode logging, bantuan baris perintah.
  • kemampuan untuk menampilkan log instruksi yang dapat dieksekusi, dekat dengan tampilan objdump ketika dibongkar.
  • kemampuan untuk menjalankan tes yang mencakup seluruh rangkaian instruksi yang diterapkan.

Program ini dibagi menjadi beberapa tahapan dan siklus:


  • baca baris perintah
  • membaca instruksi dari file ELF
  • membaca instruksi spesifik sesuai dengan penghitung PC (Program Counter) saat ini
  • instruksi decoding
  • eksekusi instruksi
  • jika terjadi situasi yang tidak terduga, jebakan diatur, memungkinkan Anda untuk menyelesaikan proses eksekusi, menandakan masalah, dan memberikan data yang diperlukan
  • jika program tidak dalam loop yang tak terbatas - tampilkan status register dan akhiri program simulasi

Apa yang termasuk dalam rencana:


  • Basis standar 64i (hampir selesai)
  • Ekstensi standar M (bilangan integer / bagi)
  • Ekstensi standar A (operasi memori atom)
  • Ekstensi standar C (Instruksi 16-bit terkompresi)
  • Ekstensi standar F (Titik apung presisi tunggal)
  • Ekstensi standar D (Titik mengambang presisi ganda * Privilege Level M (Mesin)
  • Privilege Level U (Pengguna)
  • Privilege Level S (Supervisor)
  • Skema Memori Virtual SV32, SV39 dan SV48
  • program tuan rumah
  • GPIO - bekerja dengan periferal

Bagaimana cara menjalankannya


Untuk menjalankan program, Anda harus memiliki .NET Core . Jika Anda tidak menginstalnya, maka, misalnya, di bawah Ubuntu 16.04 Anda perlu menjalankan serangkaian perintah berikut:


 $ 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 

Untuk memverifikasi bahwa sesuatu dalam hidup telah berubah, jalankan:


 $ dotnet --version 

Dan hidup harus bersinar dengan warna-warna baru!


Sekarang coba lari. Untuk melakukan ini, persediaan teh atau kopi favorit Anda, cokelat dengan roti, nyalakan musik favorit Anda dan ikuti serangkaian perintah ini:


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

dan konsol Anda akan mengedipkan mata pada Anda dengan pesan bantuan.
Peluncurannya adalah:


 $ dotnet run 

Dengan nada tegas dia akan mengatakan bahwa parameter diperlukan. Karena itu, jalankan:


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

Ini adalah momen canggung yang sama ketika ternyata kita masih membutuhkan program siap pakai untuk eksekusi untuk RISC-V. Dan ada sesuatu untuk saya bantu. Namun, Anda membutuhkan GNU toolchain untuk RISC-V . Biarkan diinstal pekerjaan rumah - deskripsi repositori menjelaskan secara cukup rinci bagaimana melakukan ini.


Selanjutnya, untuk mendapatkan file ELF tes yang didambakan, kami melakukan tindakan berikut:


 $ cd Tests/asm/ $ make build32 

jika Anda memiliki toolchain RISC-V maka semuanya akan berjalan lancar. Dan file-file tersebut harus dipamerkan di direktori:


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

dan sekarang dengan berani, tanpa melihat ke belakang, kami mencoba perintah:


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

Penting untuk dicatat bahwa Tests/asm bukan program uji, tetapi tujuan utama mereka adalah instruksi tes dan kode mereka untuk tes menulis. Oleh karena itu, jika Anda menyukai sesuatu yang lebih besar dan lebih heroik, maka mengubah dunia dalam keinginan Anda adalah menemukan file ELF 32-bit yang dapat dieksekusi secara independen yang hanya mendukung instruksi rv32i .


Namun, set instruksi dan ekstensi akan diisi ulang, menambah momentum dan menambah berat badan.


Ringkasan dan tautan


Ternyata itu adalah narasi menyedihkan yang dibumbui oleh sejarah pribadi. Terkadang teknis, kadang subjektif. Namun antusias dan dengan sentuhan antusiasme.


Bagi saya, saya tertarik untuk mendengar dari Anda: ulasan, kesan, kata perpisahan yang baik. Dan untuk yang paling berani - bantuan dalam mendukung proyek ini.


Apakah Anda tertarik dengan format naratif seperti itu dan apakah Anda ingin melanjutkan?


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


All Articles