いわゆる Parallel ML の一つである MPL の論文最新作です > Efficient Parallel Functional Programming with Effects: Jatin Arora Sam Westrick Umut A. Acar. PLDI 2023. 重要な拡張に思えたので全体を読みましたのでメモしておきます。 MPL MPL はいわ…
Rustで追実装しながら zenn.dev を読みました。 頭から読んでいけば分かる丁寧な説明だったため思ったより理解に時間は掛かりませんでした。 ただmixfix operator(そんな分類はこのアルゴリズムには無さそうだが)のbinding powerについてはもう少し説明が欲…
プログラミング言語の形式的意味論入門 を買いました。 表紙に書いてありますが The Formal Semantics of Programming Languages: an Introduction という洋書の和訳です。 多分途中で挫折しますが、とりあえず頭から眺めてみようと思います。 エラッタ 見つ…
序 Zig 言語の標準ライブラリにはジェネリックなキーバリューコンテナが含まれません。 このためZig言語用に Red-Black treeを用いた(当然ジェネリックな)コンテナライブラリ GitHub - eldesh/llrbtree-zig: A container library with llrbtree written in Z…
basis-concept-zig に続いて、Zig 言語のためのイテレータライブラリ iter-zig を作りました。 そこそこ頑張ってReadmeを書いたので詳細はそれを読むことで分かると思います。この記事には書きたいことを書きます(自明)。 Concept イテレータは、値の集合か…
Zig 言語用のライブラリ basis-concept を書きましたのでその紹介をします。 > github.com/eldesh/basis_concept 序 Zig は手続き的な型付き言語です。表現力としては、型上のコンパイル時計算によりアドホック多相を表現出来ます。ただし型コンストラクタや…
Ante という新しいプログラミング言語(とその処理系)があります。 面白そうなので勉強がてらAObenchを移植してみました: GitHub - eldesh/aobench_ante: A microbench for floating point calculation in Ante programming language 言語仕様 簡単に特徴を述…
マイクロソフト製テストケース生成ツール PICT を同僚に教えてもらいました。そのツールと、それが実装しているテスト生成アルゴリズムを紹介しているペーパー Czerwonka, Pairwise testing in real world, 2006 を読んだので、PICT とそれが採用している生…
並列MLであるMPLについての記事がsigplanのブログに投稿されていました> Provably Space-Efficient Parallel Functional Programming | SIGPLAN Blog。 面白いし論文より分かり易いので読みましょう。 MPLはSMLに並列計算のための機能を追加した並列MLの一つ…
あけましておめでとうございます。今年もよろしくお願いします。 Coqのモジュール関連の機能について和訳したので基本的な機能を紹介します。 リファレンスの文中で「対話的」モジュールとされているのは Vernacular を使って定義するからで、実体は Structu…
Coq v8.8.2 の Term の章を翻訳しました。 この章では Gallina の項の構成について説明しています。 恐らくトピックとして一番難しいのは依存型を扱うマッチ式についての説明で、詳細は別のページに独立してるくらいですが、この章で示されている例は簡潔な…
ガリグ先生の講義の9番目の資料(ssrcoq9.v)で出てくる bigop について、mathcomp.ssreflect.bigop の冒頭を訳しました*1。ssrcoq9.v の中では Notation であるはずの \big[op/idx]_~ が Definition になっていたりして混乱しますが、直接定義だけを追うより…
最近 coqtokyo 第7回Ssreflect勉強会 に参加しています。 隔週で火曜日にやっているので是非。 もうすぐ第五回講義資料(ssrcoq5.pdf)に到達しますが、ここでようやく mathcomp の話が出てきます。 さっそく opam で mathcomp をインストールしようとしたとこ…
移植 MLLex と MLYacc を Poly/ML で使えるように移植しました。 移植と言うよりは使える状態のリポジトリを作って Makefile とか書きましたというだけですが、やはりこの二つは重要なので使える状態で維持したいですね。 移植先のリポジトリは eldesh/mllex…
SMLDoc は SML# プロジェクトの一部として開発されていたドキュメント生成ツールです。 SMLコードのコメント中に書いた内容を、そのコメントに対応するエンティティに紐付けて表示するようなHTMLを生成します。昔の SML# には SMLDoc が同梱されていましたが…
SML用のユニットテストライブラリとして SMLUnit というライブラリがあります。 SML# プロジェクトの一部として開発されたようですが、現在は SML# 以外の処理系向けのコードは独立したリポジトリで管理されています。現在対応している処理系は以下の4つです…
SHA(3)はNISTが定めたセキュアなハッシュアルゴリズムの標準規格です。 今回SHA2のSML実装に続きSMLでSHA3を実装し、SHA3SMLとして公開しました。現在のところSML/NJ 110.99で動作を確認しています。 実装状況 SHA3SMLは直接FIPS 202を確認して実装しました…
POPL 2021 の論文 Provably Space-Efficient Parallel Functional Programming が出たのに合わせて2020年末*1にMaPLe v0.2 がリリースされていました。 前回の POPL の時は aobench を動かす記事 並列ML: MaPLe で AObench を高速化 を書きました。MaPLe(mpl…
前回 に引き続き JavaScript の構成要素 を読みました。 if, for, while, イベント, イベントリスナ、イベントハンドラ などが導入されました。 文中の練習問題はテキストエリアに入力されたコード片がインタラクティブにその場に反映されるというものなので…
JavaScriptを勉強することにしました。 ECMAScriptという名前で呼ばれていない時点で気にくわないものであることは確定なんですが、学ぶのが妥当という判断になってしまいました。まずMDNのJavaScriptの第一歩という教材を一通り読んで課題をやりました。 Ja…
序 CSP(Communication Sequential Process)というプロセス代数とそれに基づいた形式手法の本を読みました。頑張って読んだので紹介します。 CSPは並行計算をラベル付き遷移システムで表現した上で(これをプロセスという)、どのような遷移がありうるのか、プ…
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イメージを linux/amd64 と linux/386 のマルチアーキテクチャ対応しました。 以下のページでタグを確認すると、linux/amd64 と linux/386 という種類が表示されると思います。> eldesh/smlnj/tags 使用方法 使用する…
SMLUnitというSML用ユニットテストライブラリをPoly/ML5.8から使えるようにしました。 makeと上手く連携するMakefileが書けたので満足です。 ブランチはここ> https://github.com/eldesh/SMLUnit/tree/support/polyml *1使い方はReadmeに書いたけど、Poly/ML…
前回*1はちょっとケチが付いてしまいましたが、今回めげずに AObenchSML の SML# 版に MassiveThreads による並列化版 を追加しました。 シングルスレッド版と並列化版を両方実行します。 並列forを実装して 並列ML: MaPLe で AObench を高速化 で作ったもの…
SML# には最初からユーザレベルの細粒度スレッドライブラリ MassiveThreads のラッパーが提供されています。 Myth ストラクチャを使ってプログラムを書き、環境変数 MYTH_NUM_WORKERS で仕様コア数を指定するようです。 > 11.2 MassiveThreadsを用いた細粒度…
POPL2020 で新しい並列ML(MaPLe)(略称: MPL)の提案がありました。 正確に言うと言語の提案じゃ無くて、「並列プログラムの性質を表す(良い)性質 Disentanglement Property を提案したので、その良さ(= 並列プログラムの実行効率)を示すための処理系を作って…
Linux にはネットワークフィルタリング機能と、そのラッパーライブラリである libnetfilter-queue があります。 そのライブラリの提供するAPIである nfq_bind_pf と nfq_unbind_pf は uint16_t pf を要求します。 これに何を渡せばいいのかよく判らなかった…
github actions でビルドした内容で github pages で公開しているサイトを更新する方法をメモ。 環境+要件 案1: github-push-action 案2: actions-gh-pages 採用案 環境+要件 github 上のパブリックリポジトリである gh-pages ブランチを github pages とし…
今後覚えざるを得なさそうだったのでリポジトリを作ったついでに Github Actions を勉強して使ってみました。 勘や常識(を出来るだけ)無しに公式ドキュメントに書いてある内容のみで理解することを目標にしましたが、ちょっとつらかった。とりあえずビルドは…