サクサク読めて、アプリ限定の機能も多数!
トップへ戻る
災害への備え
keens.github.io
κeenです。お久しぶりですね。表題のとおり入社報告です。 最近はあまり入社エントリとかみなくなって悲しいですね。私もあんまり書く気なかったんですが知り合いへの連絡に便利なので残しておきます。 9/1付で入社し、コンパイラチームに配属されました。初日はアセンブラの仕様書渡されました。他にも社内ドキュメントを大量に渡されてそれ読んでるだけで1週間経ちそうです。 知り合いやTwitterでの相互フォローの方とか多いと思うのでよろしくお願いします。
# Wasmでできること、できそうなこと ---------------------- [みんなのPython勉強会#87 - connpass](https://startpython.connpass.com/event/263565/) === # About Me --------- ![κeenのアイコン](/images/kappa2_vest.png) * κeen * [@blackenedgold](https://twitter.com/blackenedgold) * [Idein Inc.](https://idein.jp/)のエンジニア * Lisp, ML, Rust, Idrisあたりを書きます * Wasm関連プロジェクト: [WebML](https://github.com/KeenS/webml)、[WebAssembler-rs](https://
← / → View PDF
κeenです。 Rustaceanのみなさんは普段書いてるRustのコードを検証するのに cargo check や cargo test などのツールを使っているかと思いますが、それらを強力にするツールの miri 、 MIRAI 、 kani をそれぞれ紹介します。 Rustにはいくつかコードの正しさや行儀のよさを検査する方法がありますね。 cargo check や cargo test 、 あるいはビルドしたバイナリを走らせて検証したり色々手を尽くしているでしょう。 ですがこれらだけだとあらゆる種類のバグを拾いきれる訳ではないのもみなさん承知の通りだと思います。 既存の方法だと手が回らない所があるので他のアプローチでコードを検証してくれるツールがあると嬉しいですよね。 そういったツールを3つ紹介します。 先に注意しておくと、これらのツールはまだ成熟しきってはおらず使いづらい点、使い
κeenです。最近バックアップを見直したのですが、その一環でtarでフルバックアップを毎週取るようにしたのでその報告です。 背景 今までUbuntuに標準でついてきたdeja-dupを使っていたのですが、リモートストレージにバックアップを取れない、リストアが遅い、使用するストレージ容量の上限を設定できない、などの理由で乗り換えを検討しました。 調査の結果、1つのツールで条件を満たすのは難しそうなので用途別にバックアップを使い分けることにしました。ここではその用途の1つ、「家が燃えるなどしてPCのデータが一切ダメになった場合に備えた完全なバックアップ」を取るための方法です。 検討したときのスクラップはこちらにあります。 バックアップを考えたい やりたいこと データが一切ダメになって、復元するときも全てのデータを丸ごと復元するケースを想定しているので割り切った要求になります 毎回フルバックアッ
κeenです。Rustではじめてアプリケーションを書くときに困りがちなことの1つにグローバルな値を持つにはどうしたらいいか分からないというのがあるようです。 その書き方を何パターンか紹介しできたらなと。 一応この記事には元ネタというかインスパイア元があり、以下のリポジトリも見ながら書かれています。 https://github.com/paulkernfeld/global-data-in-rust let にする 一番よくあるケースだとCLIや起動時に読み込んだ設定ファイルの値をどうするかでしょう。データの性格として起動時に一度だけ生成してあとは(ほとんど)いじらないようなものです。そういうものは main 関数内で let して、あとは借用で持ち回ればよいです。 起動時にファイルかろ設定値を読み込んで動くアプリケーションを雰囲気で書くとこんな感じです。 use std::io; str
κeenです。昨日Ubuntu 22.04に上げたら色々問題が起きたので私がやった解決策を残しておきます。 グラフィックドライバの問題(多分) 問題 dist upgrade時にグラフィックドライバ系のパッケージでインストールエラーが発生しました。 これは恐らく私がUbuntu標準でないAMDが配布しているドライバをインストールしていたからだと思います。 ただ、そのせいか再起動するとGUIが立ち上がらず、画面が黒いままになってしまいました。 解決 一旦AMDのグラフィックドライバをアンインストールして、GUIに関係ありそうな gdm3 や ubuntu-session 、mutter などを再インストールしました。 アンインストールは、黒い画面で `Ctrl + Alt + F1~F12`` のどれかを押すとコンソールに行けるのでそこでログインしてターミナルで操作しました。 以下のようなコ
κeenです。表題のとおりのことをやりたかったのですが、ピンポイントのAPIが見当らなかったのでやり方を書き留めます。 2022-02-22: 末尾に追記しました やりたいこととしてはCとのFFIをやっていて要素列へのポインタと要素数があるときに、それをRustの世界に持ち込みたいというもの。 コードはこういう感じですね。 use std::ffi::c_void; use std::mem; extern "C" { fn calloc(nmemb: usize, size: usize) -> *mut c_void; } fn main() { unsafe { let nitems = 512; let ptr = calloc(nitems, mem::size_of::<i32>()); // ↑このポインタを `Box<[i32]>` として扱いたい } } use std:
κeenです。以前の記事の続きで、 /proc を監視するのではなくeBPFで取得してみます。ついでにRustのコードをeBPFで動かせるライブラリのayaも使ってみます。 以前の記事では /proc 以下の監視をビジーループで回すという力技で新しく作られたプロセスを補足していました。これだとCPU使用率が上がって美しくありませんし、何より原理的には見逃しもありえてしまいます。そこでカーネルの機能を使って全てのプロセスの作成を監視して低CPU使用率かつ捕捉率100%の実装を目指します。 eBPFとは? なんかLinuxカーネルでユーザの書いたコード動かせるやつです。私は説明できるほど詳しくないので適当にググって下さい。 1つやっかいな点として、独自のバイナリを動かすのでカーネル内で動かすコードはコンパイラがeBPFに対応したものでないといけません。また、カーネル内で動かすコードをユーザラン
このエントリはRust Advent Calendarの2日目の記事です。 空いてる日を埋める担当のκeenです。2日目が空いてたので遡って記事を投稿します。 最近v1.0.0がリリースされたリンカ、moldを使うとビルドが高速化するよというお話です。 Rustのビルド、特にインクリメンタルビルドにおいてはRustコンパイラの速さと同じくらいリンカの速度がコンパイル時間に影響します。 この最後のバイナリを作る時間は意外と効いてきます。 具体例としてActix Webにあるexample、 basic をインクリメンタルビルドする例をみてみましょう。 この basic はたった42行の小さなアプリケーションです。 ただし、依存に Actix Webという巨大なライブラリを使っているので最終的なバイナリには非常に多くのコードが含まれます。フレームワークを使ってアプリケーションを開発してるときに
κeenです。SML# 3.7.0から実験的機能として _dynamiccase に存在型のサポートが入ったので試してみます。 本記事はSML# 4.0.0 with LLVM 12.0.0で動作確認を行っています。 Dynamicについて _dynamiccase 以前にDynamicの説明から入りましょう。 DynamicはSML# 3.5.0から入った機能です。 型を消して代わりにデータに埋め込んでおき、使うときにその型を復元して使えるものです。 型を消す(型をデータに埋め込む)のは Dynamic.dynamic などのプリミティブを、型を復元するのは _dynamic などの制御構造を使います。 val x = Dynamic.dynamic {a = 1, b = "c"} (* val x = _ : Dynamic.void Dynamic.dyn *) val y = _
# Idris2の数量的型が解決した問題導入した問題 ---------------------- [第一回関数型プログラミング(仮)の会 - connpass](https://opt.connpass.com/event/222709/) === # About Me --------- ![κeenのアイコン](/images/kappa2_vest.png) * κeen * [@blackenedgold](https://twitter.com/blackenedgold) * GitHub: [KeenS](https://github.com/KeenS) * GitLab: [blackenedgold](https://gitlab.com/blackenedgold) * [Idein Inc.](https://idein.jp/)のエンジニア * Lisp, ML
κeenです。コンパイル時に定数を処理する最適化技法あるじゃないですか。あれの名称がイマイチはっきりしないのでモヤモヤするなーという記事です。 技法 コンパイル時に定数を処理する最適化技法は色々あるんですがそれらを包括した名称だったり個別の名称だったりがごっちゃになってるのがはっきりしない要因です。 ここでは個別の技法を7つ挙げておきます。 技法A 定数と分かっている変数を定数におきかえるやつ 例 A = 100; B = A + 10; ↓ A = 100; B = 100 + 10; 技法B 変数から変数への代入を削除し、代入先の変数への参照を代入元の変数への参照に置き換えるやつ 例 A = 100; B = A; C = B + 10; A = 100; C = A + 10; 技法C 条件分岐の条件が定数の場合に条件なしジャンプにするやつ 例 if (true) { do_some
κeenです。漢字変換高精度に行うためにSKK辞書をいくつか作ったので報告です。 辞書 GitHubに上げています。手元にダウンロードして各々好きなように使って下さい。ライセンスはCC BY-SA 3.0です。 SKK_JISYO.wiktionary 解決したい問題と対応する辞書 SKKに限らずほとんどの日本語での漢字変換は読みを入力してそれに該当する候補から漢字を選択していると思います。この方法は直感的で分かりやすいのですが、私は2つ問題を感じています。 同じ読みに対する候補が多すぎる 読みが分からない漢字を変換できない 1の候補の数については特に音読の入力に対して顕著です。例えば「しょう」で変換するとSKK_JISYO.Lにある候補は174あり、その中から目的の漢字を目grepで探す作業がはじまります。変換したい漢字は思い浮かんでいるはずなので、この目grepはインタフェースが洗練さ
κeenです。ちょっと気紛れでCPUの拡張命令を使ってみようかなと思ったのでRustから叩いてみます。 Rustから叩くとはいってもあんまり難しいものではなくて、intrinsicsとして実装されているのでそれを呼ぶだけです。今回はBMI2拡張のPDEP/PEXTを呼んでみます。 PDEP/PEXT BMI(Bit Manipulation Instruction Set)はその名のとおりビット操作を提供するx86の拡張命令です。IntelのHaswellから導入されてAMDのCPUもサポートしているようです。ABM、 BMI1、 BMI2と関連する拡張が色々あってややこしいので詳しくはWikipediaの記事を参考にして下さい。今回はBMI2を使います。その中のPDEP/PEXTはビットフラグ関連の操作を提供します。PEXTは「ビットマスクでマスクしてシフトでLSBに移動」、PDEPは逆
κeenです。最近YubiKeyを買ったので色々試しています。今回はそのうちのLinuxログイン回です。 YubiKeyについて YubiKeyは米瑞企業のYubico社が販売している認証デバイスです。FIDOやらWebAuthnやらの文脈で耳にした方も多いんじゃないしょうか。YubiKeyは日本ではソフト技研社が販売代理店をしています。 YubiKeyはラインナップがいくつかありますが私が買ったのはYubiKey 5 NFCです。 YubiKeyでできることは色々あります。 FIDO U2F FIDO2 / WebAuthn Challenge and Response OATH-TOTP / OATH-HOTP Yubico OTP PIV OpenPGP 静的パスワード 参考:Yubikey 5をArchLinuxで使う - Qiita このうち今回はFIDO U2F、Challen
κeenです。最近YubiKeyを買ったので色々試しています。今回はそのうちのWeb認証回です。 YubiKeyについて YubiKeyは米瑞企業のYubico社が販売している認証デバイスです。FIDOやらWebAuthnやらの文脈で耳にした方も多いんじゃないしょうか。YubiKeyは日本ではソフト技研社が販売代理店をしています。 YubiKeyはラインナップがいくつかありますが私が買ったのはYubiKey 5 NFCです。 YubiKeyでできることは色々あります。 FIDO U2F FIDO2 / WebAuthn Challenge and Response OATH-TOTP / OATH-HOTP Yubico OTP PIV OpenPGP 静的パスワード 参考:Yubikey 5をArchLinuxで使う - Qiita このうち今回はFIDO U2F、FIDO/WebAut
κeenです。最近Yubikeyを買ったので色々試しています。今回はそのうちのPGP回です。 Yubikeyについて Yubikeyは米瑞企業のYubico社が販売している認証デバイスです。FIDOやらWebAuthnやらの文脈で耳にした方も多いんじゃないしょうか。Yubikeyは日本ではソフト技研社が販売代理店をしています。 Yubikeyはラインナップがいくつかありますが私が買ったのはYubikey 5 NFCです。 Yubikeyでできることは色々あります。 FIDO U2F FIDO/WebAuthn Challenge and Response OATH-TOTP / OATH-HOTP Yubico OTP PIV OpenPGP 静的パスワード 参考:Yubikey 5をArchLinuxで使う - Qiita このうち今回はOpenPGPサポートの機能を使います。 Open
M.2のNVMe SSD x 4の上にbtrfsでRAID 5を組んだファイルシステム上で実験しており、Linuxカーネルは5.8.0でした。 公平性の調整 ネタバレになるですが、キャッシュの具合やファイルが残ってるかどうかで速度が結構変わるのでベンチマーク後にファイルは削除し、ベンチマークの間に sync() を挟むことでキャッシュの影響をなくすようにしました。 Linuxのアップデート 本件とは別の事情で最新版のLinuxを使う用事が発生したのでLinux 5.11.0を使っています。リリースノートを見るとbtrfsの高速化なども含んでいるので一応ベンチマークを取り直してみます。 name time(ms)
κeenです。普段お世話になってるけど使ったことのないAPIを叩いてみよう、ということで io_uring を使ってみます。 io_uringが何なのかは以下の記事が詳しかったです。 Linuxにおける非同期IOの実装について - Qiita ざっくり、io_uringはLinuxで非同期IOをするためのAPIです。 ユーザランドとカーネルランドで2つのキューを共有し、そこを通じて会話をします。 1つのキューはユーザランドからカーネルへのリクエストの提出用、もう1つのキューはカーネルからユーザランドへの完了の通知用です。 また、epollを制御するためにfdもあります。こんなイメージですかね。 user | ^ ^ submit ||| || ||| completion -------|||--fd-|||---------- ||| || ||| v v | kernel それぞれのキ
κeenです。 普段お世話になってるけど使ったことのないAPIを叩いてみよう、ということで epoll(7) を使ってみます。 Epollとは epoll(7) はLinux固有のAPIで、パイプやソケットなど出入力に待ちが発生する対象を複数同時に待つ、いわゆるIOの多重化の機能を提供します。 同等のことをするAPIはUNIX全般で使える select(2) や poll(2) などもありますが、使い勝手やパフォーマンスの面で epoll が勝るようです。 一方で epoll(7) はLinux固有のAPIなのでmacOSやFreeBSDでは使えません。それらのOSでは別のAPI(kqueue(2))を叩くことになります。 Rustならmioが互換レイヤとして存在し、LinuxでもBSDでもmacOSでも使えるライブラリになっています。 mioはTokioなんかで使われていますね。ですが今
κeenです。最近JEITAのソフトウェアエンジニアリング技術ワークショップ2020に参加したんですが、そこで五十嵐先生、柴田さん、Matzとパネルティスカッションをしました。その議論が面白かったので個人的に話を広げようと思います。 年末年始休暇に書き始めたんですが体調を崩したりと色々あって執筆に時間がかかってしまいました。 時間を置いて文章を書き足していったので継ぎ接ぎ感のある文体になってるかもしれませんがご容赦下さい。 というのを踏まえて以下をお読み下さい。 いくつか議題があったのですが、ここで拾うのは一番最後の「プログラミング言語の未来はどうなるか」という話題です。 アーカイブが1月末まで残るようです。もうあと数日しかありませんが間に合うかたはご覧下さい。 そのとき各人の回答を要約すると以下でした。 五十嵐先生:DSLを簡単に作れる言語というのが重要。それとプログラム検証、プログラム
このエントリはIdris Advent Calendar 2020の19日目の記事です。 次はmock_beginnerさんでIdrisとはじめる型駆動開発です。 κeenです。今回はこのAdvent Calendarの山場の1つ、定理証明について解説しようと思います。 依存型で証明ができる原理 カリー=ハワード同型対応といって、プログラムのと論理学の定理には対応関係があることが知られています。 これはすなわち、我々が普段プログラムを書いているときは同時に論理学の命題を証明していることでもある、ということです。 そんな大それたことしてないよーと思うかもしれませんが、それもそのはず。 普通のプログラムではあまり面白い命題を表現できないので、わざわざ証明というほどでもないからです。 しかしIdrisには依存型があります。 依存型があると型の表現力が上がるので対応する論理学の命題の表現力が上がり
error[E0010]: allocations are not allowed in constants --> const.rs:1:23 | 1 | const VEC: Vec<i32> = vec![1]; | ^^^^^^^ allocation not allowed in constants | = note: this error originates in a macro (in Nightly builds, run with -Z macro-backtrace for more info) この制限された static や const の右辺に書くときの文脈を const文脈 と呼びます。 この他には配列初期化構文 [init; size] の size の部分やその型 [Type; Size] の Size 、あとはC-like列挙型の判別子の設定に書ける式も
# Rust with Fearless Concurrency ---------------------- === # About Me --------- ![κeenのアイコン](/images/kappa2_vest.png) * κeen * [@blackenedgold](https://twitter.com/blackenedgold) * GitHub: [KeenS](https://github.com/KeenS) * GitLab: [blackenedgold](https://gitlab.com/blackenedgold) * [Idein Inc.](https://idein.jp/)のエンジニア * Lisp, ML, Rust, Shell Scriptあたりを書きます === # Rust with Fearless Concurrency
たまに得体の知れないコマンドシェルスクリプトを直接 sh に流すのを嫌う人がいますが、 そもそも得体のしれないバイナリ(rustコンパイラ)をインストールしようとしてるので気にしすぎでしょう。 さて、上記コマンドを実行すると以下のようにインストールが走ります。 info: downloading installer Welcome to Rust! This will download and install the official compiler for the Rust programming language, and its package manager, Cargo. Rustup metadata and toolchains will be installed into the Rustup home directory, located at: /home/shun/
import Data.String data FizzBuzz = F | B | FB | I Integer Show FizzBuzz where show F = "fizz" show B = "buzz" show FB = "fizzbuzz" show (I n) = show n fizzBuzz : Integer -> FizzBuzz fizzBuzz n = case (n `mod` 3, n `mod` 5) of (0, 0) => FB (_, 0) => B (0, _) => F _ => I n fizzBuzzSeq : Integer -> List FizzBuzz fizzBuzzSeq n = map fizzBuzz [1..n] main : IO () main = do [_, arg] <- getArgs | _ => put
このエントリは言語実装 Advent Calendar 2020の1日目の記事です。 次はsisshiki1969さんで「RustでつくるRuby、その後の進捗」です。 κeenです。 昔からちまちま作ってるSML処理系をブラウザ上で動かすことができたのでその進捗報告です。 ちまちま作ってるSML処理系とはこれのことです。 KeenS/webml: A Standard ML Compiler for the Web 今回実装したオンラインコンパイラは以下で試すことができます: WebML Online Compiler まあ、ブラウザで動くのでここに貼ることもできるんですけどね。 こういうのどうやって作ったの?っていうのを話していけたらなと思います。 設計 そもそもの話、WebMLはブラウザで動かすために設計、実装されています。 スタートから違うじゃんと思うかもしれませんが、スタートから
κeenです。めずらしくWebの話題でも。ブラウザ上で音出したいときってどうすればいいんだっけとなって調べた結果です。 Web Audio API 個人的にはSVGのオーディオ版の、楽譜っぽいものをテキストで入力したら勝手に音が鳴ってくれるフォーマットをさがしてたのですがみつかりませんでした(辛うじてMusicXMLが近いくらい?)。MIDIとかにも期待したんですがあれはバイナリ 代わりに、Web Audio APIというのを使えばブラウザ上で音が出せそうというのがみつかりました。 Web Audio API - Web APIs | MDN この中の OscillatorNode を使えば手で音が出せそうです。 OscillatorNode OscillatorNode を使ったサンプルを実装してみたのがこれ(クリックすると大きめの音が鳴ります)。 <div id="oscPlayer"
次のページ
このページを最初にブックマークしてみませんか?
『Lispエイリアンの狂想曲 | κeenのHappy Hacκing Blog』の新着エントリーを見る
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く