Location via proxy:   [ UP ]  
[Report a bug]   [Manage cookies]                

タグ

cとosに関するmasterqのブックマーク (3)

  • The Pip Protokernel

    masterq
    masterq 2024/11/27
    "The logic of Pip is implemented in Gallina — the language of the Coq proof assistant — and it is in the process of being equipped with a formal proof that it ensures memory isolation. For efficiency, it is automatically translated into freestanding C code."
  • The Pip Protokernel

    masterq
    masterq 2017/05/01
    わずか9つしかシステムコールのないkernel。ユーザ空間の上でLinuxとFreeRTOSが同時に動く。今はx86実装のみ。Xenのさらに薄い版みたいな感じ?Coqで証明済み。副作用はモナドで抽象化し、ポインタ使用も安全だとのこと
  • 非同期入出力の残念な現状

    asynchronous disk I/O | libtorrent blog Libtorrent experience - the poor state of async disk IO | Hacker News libtorrentの作者が、ディスクI/Oをパフォーマンスを向上させるために非同期I/Oを試した結果、どの環境でも残念なので、ブロックI/Oをスレッドプールで行う擬似非同期I/Oで実装したとブログを書いている。その問題について、Hacker Newsでも議論されている。 非同期I/Oは、話を聞くとたのもしい機能に思える。読み書きが完了するまでブロックせずに、完了したらOSが通知するという仕組みだ。 問題は、その実装がどの環境でも貧弱だという事だ。 環境というのは、主にOS側のことだ。多くのモダンなOSは非同期I/Oを提供している。特に著名なのがみっつある。 Linux A

    masterq
    masterq 2012/10/28
    "読み書きやバッファやサイズなどは、512バイトに正しくアライメントされていなければならない。これを正しく行うのは、恐ろしい手間がかかる"全く同意できない。これだから...
  • 1