Efficient Parallel Functional Programming with Effects を読んだ

いわゆる Parallel ML の一つである MPL の論文最新作です > Efficient Parallel Functional Programming with Effects: Jatin Arora Sam Westrick Umut A. Acar. PLDI 2023. 重要な拡張に思えたので全体を読みましたのでメモしておきます。 MPL MPL はいわ…

Prattパーサの記事を読んだ

Rustで追実装しながら zenn.dev を読みました。 頭から読んでいけば分かる丁寧な説明だったため思ったより理解に時間は掛かりませんでした。 ただmixfix operator(そんな分類はこのアルゴリズムには無さそうだが)のbinding powerについてはもう少し説明が欲…

プログラミング言語の形式的意味論入門を買った

プログラミング言語の形式的意味論入門 を買いました。 表紙に書いてありますが The Formal Semantics of Programming Languages: an Introduction という洋書の和訳です。 多分途中で挫折しますが、とりあえず頭から眺めてみようと思います。 エラッタ 見つ…

Zig言語用コンテナライブラリ llrbtree-zig を実装しました

序 Zig 言語の標準ライブラリにはジェネリックなキーバリューコンテナが含まれません。 このためZig言語用に Red-Black treeを用いた(当然ジェネリックな)コンテナライブラリ GitHub - eldesh/llrbtree-zig: A container library with llrbtree written in Z…

Zig 言語用のイテレータライブラリを書きました

Zig

basis-concept-zig に続いて、Zig 言語のためのイテレータライブラリ iter-zig を作りました。 そこそこ頑張ってReadmeを書いたので詳細はそれを読むことで分かると思います。この記事には書きたいことを書きます(自明)。 Concept イテレータは、値の集合か…

Zig 言語用ライブラリ basis-concept を書きました

Zig

Zig 言語用のライブラリ basis-concept を書きましたのでその紹介をします。 > github.com/eldesh/basis_concept 序 Zig は手続き的な型付き言語です。表現力としては、型上のコンパイル時計算によりアドホック多相を表現出来ます。ただし型コンストラクタや…

AnteでAObenchを書いた

Ante という新しいプログラミング言語(とその処理系)があります。 面白そうなので勉強がてらAObenchを移植してみました: GitHub - eldesh/aobench_ante: A microbench for floating point calculation in Ante programming language 言語仕様 簡単に特徴を述…

t-wise testing 入門

マイクロソフト製テストケース生成ツール PICT を同僚に教えてもらいました。そのツールと、それが実装しているテスト生成アルゴリズムを紹介しているペーパー Czerwonka, Pairwise testing in real world, 2006 を読んだので、PICT とそれが採用している生…

sigplanブログにMPLの記事が投稿されていた

並列MLであるMPLについての記事がsigplanのブログに投稿されていました> Provably Space-Efficient Parallel Functional Programming | SIGPLAN Blog。 面白いし論文より分かり易いので読みましょう。 MPLはSMLに並列計算のための機能を追加した並列MLの一つ…

Coqのモジュールの基本機能

Coq

あけましておめでとうございます。今年もよろしくお願いします。 Coqのモジュール関連の機能について和訳したので基本的な機能を紹介します。 リファレンスの文中で「対話的」モジュールとされているのは Vernacular を使って定義するからで、実体は Structu…

CoqのマニュアルのTermの章を翻訳した

Coq v8.8.2 の Term の章を翻訳しました。 この章では Gallina の項の構成について説明しています。 恐らくトピックとして一番難しいのは依存型を扱うマッチ式についての説明で、詳細は別のページに独立してるくらいですが、この章で示されている例は簡潔な…

mathcomp bigop 概要を和訳

Coq

ガリグ先生の講義の9番目の資料(ssrcoq9.v)で出てくる bigop について、mathcomp.ssreflect.bigop の冒頭を訳しました*1。ssrcoq9.v の中では Notation であるはずの \big[op/idx]_~ が Definition になっていたりして混乱しますが、直接定義だけを追うより…

opamでmathcompをインストールした

最近 coqtokyo 第7回Ssreflect勉強会 に参加しています。 隔週で火曜日にやっているので是非。 もうすぐ第五回講義資料(ssrcoq5.pdf)に到達しますが、ここでようやく mathcomp の話が出てきます。 さっそく opam で mathcomp をインストールしようとしたとこ…

MLLex と MLYacc を Poly/ML に移植

SML

移植 MLLex と MLYacc を Poly/ML で使えるように移植しました。 移植と言うよりは使える状態のリポジトリを作って Makefile とか書きましたというだけですが、やはりこの二つは重要なので使える状態で維持したいですね。 移植先のリポジトリは eldesh/mllex…

SML のドキュメント生成ツール SMLDoc をサルベージした

SML

SMLDoc は SML# プロジェクトの一部として開発されていたドキュメント生成ツールです。 SMLコードのコメント中に書いた内容を、そのコメントに対応するエンティティに紐付けて表示するようなHTMLを生成します。昔の SML# には SMLDoc が同梱されていましたが…

SMLUnit のインストールを統一して簡潔にした

SML

SML用のユニットテストライブラリとして SMLUnit というライブラリがあります。 SML# プロジェクトの一部として開発されたようですが、現在は SML# 以外の処理系向けのコードは独立したリポジトリで管理されています。現在対応している処理系は以下の4つです…

SMLでSHA3を実装しました

SML

SHA(3)はNISTが定めたセキュアなハッシュアルゴリズムの標準規格です。 今回SHA2のSML実装に続きSMLでSHA3を実装し、SHA3SMLとして公開しました。現在のところSML/NJ 110.99で動作を確認しています。 実装状況 SHA3SMLは直接FIPS 202を確認して実装しました…

並列ML: MaPLe v0.2 がリリースされていた

POPL 2021 の論文 Provably Space-Efficient Parallel Functional Programming が出たのに合わせて2020年末*1にMaPLe v0.2 がリリースされていました。 前回の POPL の時は aobench を動かす記事 並列ML: MaPLe で AObench を高速化 を書きました。MaPLe(mpl…

MDN の JavaScript building blocks を読み終えた

前回 に引き続き JavaScript の構成要素 を読みました。 if, for, while, イベント, イベントリスナ、イベントハンドラ などが導入されました。 文中の練習問題はテキストエリアに入力されたコード片がインタラクティブにその場に反映されるというものなので…

MDN の JavaScript First Steps を読んだ

JavaScriptを勉強することにしました。 ECMAScriptという名前で呼ばれていない時点で気にくわないものであることは確定なんですが、学ぶのが妥当という判断になってしまいました。まずMDNのJavaScriptの第一歩という教材を一通り読んで課題をやりました。 Ja…

並行システムの検証と実装を読んだ

序 CSP(Communication Sequential Process)というプロセス代数とそれに基づいた形式手法の本を読みました。頑張って読んだので紹介します。 CSPは並行計算をラベル付き遷移システムで表現した上で(これをプロセスという)、どのような遷移がありうるのか、プ…

SML#のDockerイメージが全種揃った

eldesh/smlsharp で公開しているSML#のdockerイメージがあります。 最近必要になって バージョン1 系列(1.0.0, 1.0.1, 1.0.2, 1.0.3, 1.1.0)を追加しました。今月初め頃 0.90 をビルドしてあったため、 これで現時点でのリリースを全種揃えたことになりまし…

SML/NJのdockerイメージをマルチアーキテクチャ対応した

私が個人的に管理しているsml/njのdockerイメージを linux/amd64 と linux/386 のマルチアーキテクチャ対応しました。 以下のページでタグを確認すると、linux/amd64 と linux/386 という種類が表示されると思います。> eldesh/smlnj/tags 使用方法 使用する…

SMLUnitをPoly/MLに対応した

SMLUnitというSML用ユニットテストライブラリをPoly/ML5.8から使えるようにしました。 makeと上手く連携するMakefileが書けたので満足です。 ブランチはここ> https://github.com/eldesh/SMLUnit/tree/support/polyml *1使い方はReadmeに書いたけど、Poly/ML…

SML# 版 AObench をMassiveThreadsで高速化

SML

前回*1はちょっとケチが付いてしまいましたが、今回めげずに AObenchSML の SML# 版に MassiveThreads による並列化版 を追加しました。 シングルスレッド版と並列化版を両方実行します。 並列forを実装して 並列ML: MaPLe で AObench を高速化 で作ったもの…

SML#のプログラムにMassiveThreadsのオプションを付けるとパフォーマンスが低下する

SML

SML# には最初からユーザレベルの細粒度スレッドライブラリ MassiveThreads のラッパーが提供されています。 Myth ストラクチャを使ってプログラムを書き、環境変数 MYTH_NUM_WORKERS で仕様コア数を指定するようです。 > 11.2 MassiveThreadsを用いた細粒度…

並列ML: MaPLe で AObench を高速化

SML

POPL2020 で新しい並列ML(MaPLe)(略称: MPL)の提案がありました。 正確に言うと言語の提案じゃ無くて、「並列プログラムの性質を表す(良い)性質 Disentanglement Property を提案したので、その良さ(= 並列プログラムの実行効率)を示すための処理系を作って…

nfq_bind_pf の使い方

Linux にはネットワークフィルタリング機能と、そのラッパーライブラリである libnetfilter-queue があります。 そのライブラリの提供するAPIである nfq_bind_pf と nfq_unbind_pf は uint16_t pf を要求します。 これに何を渡せばいいのかよく判らなかった…

GitHub Actions で Github Pages を更新する方法

github actions でビルドした内容で github pages で公開しているサイトを更新する方法をメモ。 環境+要件 案1: github-push-action 案2: actions-gh-pages 採用案 環境+要件 github 上のパブリックリポジトリである gh-pages ブランチを github pages とし…

Github Actions を勉強した

今後覚えざるを得なさそうだったのでリポジトリを作ったついでに Github Actions を勉強して使ってみました。 勘や常識(を出来るだけ)無しに公式ドキュメントに書いてある内容のみで理解することを目標にしましたが、ちょっとつらかった。とりあえずビルドは…