サクサク読めて、アプリ限定の機能も多数!
トップへ戻る
中東情勢
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です。今年のエイプリルフールのジョークのGPUを用いたFizzBuzzの高速化の取り組みについて解説します。 今年のテーマはGPUで、最近GPUプログラミングを勉強してるのでその成果発表会も兼ねています。メインのジョークとしては特に高速化する意味のないプログラムを、特に向いていないGPUで高速化したと主張するものです。サブのジョークとして筋の悪い論文のように論拠に欠けていたり何をしたかったのか分からなかったりする内容を目指しました。みなさんも読んでいても心の中で突っ込んだ箇所は数知れないと思います。これの元ネタとしてはTwitterでみかけた「ラーメンにアイスクリームをのっけたような論文」があったのですが、今探したら元ネタのツイートがみあたりませんでした。 コードの速度とか さて、少し真面目にプログラムを解説しましょう。なんとなくFizzBuzzをGPUで実行しても速くならんだろ、
κ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です。よくある言語同士や言語実装同士の速さの比較に使われるベンチマークが実際にどんなところの性能を調べているのかを理解してないので軽く調べてみます。 色々調べようかと思ったんですが、一番よく見るのはComputer Language Benchmarks Gameの結果かなと思うのでここで使われているベンチマーク10種について調べていきます。 調べるとはいっても説明を読んで、ベンチマークに使われてるプログラムを読んで感想を言っていくだけです。実際にプロファイルをとってどこがボトルネックになるとかまではやらずに想像で喋ってるので参考程度に見ていって下さい。 fannkuch-redux fannkuch-reduxは数字列を操作するプログラムです。 求める計算は以下です ${1,\cdots,n}$の並べ替えを受け取る 例: ${4,2,1,5,3}$ 最初の要素を見て(ここでは4)
κ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さんだよー。今日は年度が変わって大学でプログラミングをはじめたり、新卒でプログラマになったりする人もいるでしょうということでアヴィウムプルヌスについて解説したいと思います。アヴィウムプルヌスは慣れると便利に使えますが最初はとっつきにくいですよね。 アヴィウムプルヌスとは 普通のプルヌスなら分かりますけどアヴィウムってついたらよく分かりませんよね。でも怖がらなくて大丈夫です。アヴィウムプルヌスも普通のプルヌスです。ただしラパにプルヌスをとります。プルヌスの中でもラパにプルヌスをとるものをアヴィウムプルヌスと呼ぶのです。 今の説明で「なるほど分かった」と納得した方もいるかもしれませんが「余計に訳が分からなくなった」という方の方が多いんじゃないでしょうか。順を追って説明しましょう。 アヴィウムプルヌスは何をしているのか さきほどアヴィウムプルヌスはプルヌスをラパにとるプルヌスと説
κ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
κeenです。数年ブログをやってきて記事が溜まったので目的の記事をさがしやすいように全文検索をつけてみました。 このページです。右上のsearchから飛べます。実装は至ってシンプルで、本当に全文を検索しているだけです。ですがここに至るまでにちょっと経緯があったので紹介します。 候補の検討 このissueでいくつか検討しています。私のブログは静的サイトジェネレータのHugoで作られているのでサーバで動作するコードはありません。全てをフロントエンドでやる必要があります。全文検索はフロントエンドでやるには少し重いタスクですが最近だとWebAssemlyがあるので徐々にフロントエンド全文検索が浸透してきているようです。 今回検討の元になったというか全文検索を載せようと思ったのは以下の記事が発端です。 WebAssembly Search Tools for Static Sites — Andre
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を簡単に作れる言語というのが重要。それとプログラム検証、プログラム
κeenです。 去年末にhatsugaiさんが面白い問題を出してたのでIdrisで解いてみます。 大晦日クイズ P は自然数についての述語 pic.twitter.com/YfaI2QyNeS — hatsugai ∈ PRINCIPIA (@hatsugai) December 31, 2020 Twitterの埋め込み画像を見れない人のためにこちらにも書くとこういう命題を証明せよという問題です。 \[ (\forall n. P(n) \implies \exists m. m \lt n \land P(m)) \implies \lnot \exists n. P(n) \] これは無限降下法とよばれる原理です。 自然言語で書くと、「「任意の $n$ について、 $P(n)$ ならば $m \lt n$ なる $m$ が存在して $P(m)$ となる」ならば $P(n)$ となる
このエントリはIdris Advent Calendar 2020の19日目の記事です。 次はmock_beginnerさんでIdrisとはじめる型駆動開発です。 κeenです。今回はこのAdvent Calendarの山場の1つ、定理証明について解説しようと思います。 依存型で証明ができる原理 カリー=ハワード同型対応といって、プログラムのと論理学の定理には対応関係があることが知られています。 これはすなわち、我々が普段プログラムを書いているときは同時に論理学の命題を証明していることでもある、ということです。 そんな大それたことしてないよーと思うかもしれませんが、それもそのはず。 普通のプログラムではあまり面白い命題を表現できないので、わざわざ証明というほどでもないからです。 しかしIdrisには依存型があります。 依存型があると型の表現力が上がるので対応する論理学の命題の表現力が上がり
このエントリはIdris Advent Calendar 2020の18日目の記事です。 κeenです。Idrisで個人的に面白いなーと思ってる機能、 with 構文とそれを利用したViewについて紹介します。 パターンマッチを補助する with 構文 関数を書くときに条件分岐したくなることがありますよね。 データ型の構造に沿う条件であれば引数でのパターンマッチで済むんですが、もう少し複雑な条件だと if や case を使わざるを得なくなります。 例えば「リストに値がなければ追加する」関数 addToList はこう書けるでしょう。 addToList : Eq a => a -> List a -> List a addToList x xs = if elem x xs then xs else x::xs こういうのも引数のパターンマッチで書けると綺麗ですよね。 これは with
次のページ
このページを最初にブックマークしてみませんか?
『Lispエイリアンの狂想曲 | κeenのHappy Hacκing Blog』の新着エントリーを見る
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く