[go: up one dir, main page]

タグ

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

  • TinyOS - Wikipedia

    TinyOS is an embedded, component-based operating system and platform for low-power wireless devices, such as those used in wireless sensor networks (WSNs), smartdust, ubiquitous computing, personal area networks, building automation, and smart meters. It is written in the programming language nesC, as a set of cooperating tasks and processes. It began as a collaboration between the University of C

    TinyOS - Wikipedia
  • 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