作者別: Jun Mukai

仕様検証言語 TLA+ の AWS における使用事例について向井が話します。感想などはハッシュタグ #misreading か hello@misreading.chat にお寄せください。

• Why Amazon Chose TLA +  | SpringerLink (Google Scholar)
  • How Amazon Web Services Uses Formal Methods
• Practical TLA+: Planning Driven Development: Hillel Wayne
• Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers: Leslie Lamport
• TLA+tlaplus/tlaplus: TLC is an explicit state model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.

Follow up

• Grenade! Dependently Typed Neural Networks — Monday Morning Haskell
• ハイパーバイザの作り方
• エンジニアなら知っておきたい仮想マシンのしくみ：連載｜gihyo.jp … 技術評論社

FreeBSD のサンドボックス機構 Capsicum について向井が話します。

• Capsicum: practical capabilities for UNIX
• Capsicum – FreeBSD Wiki
• Computer Laboratory: Capsicum: practical capabilities for UNIX
• Capsicum and Casper – a fairy tale about solving security problems
• Capsicum | Hacker News
• Pledge: OpenBSD’s defensive approach to OS Security

Follow up

• Mitsutoshi Aoe/maoe on Twitter: “#misreading ep. 41でIdrisの話をしてた。最近作者は https://t.co/PANlfh8SC1 というIdris 2のプロトタイプを作っているので、これが一番実用的なアプリケーションになるのかなあ。”
  • edwinb/Blodwen: A prototype successor to Idris
• Manning | Type-Driven Development with Idris

汎用プログラミング言語に Dependent Types を組み込んだ実験的なプログラミング言語 Idris について向井が話します。

感想などはハッシュタグ #misreading か hello@misreading.chat にお寄せください。

• IDRIS — Systems Programming Meets Full Dependent Types (PDF)
• Idris | A Language with Dependent Types
• Kazuyoshi Kato on Twitter: “最近の言語で dependent types… 多分 Idris じゃないかと https://t.co/tRLdzd0KAr #misreading”

Follow up

• skip · A programming language to skip the things you have already computed
• Chromeのメモリ割り当てフック機構 – kanejaku.org

ニューラル自然言語処理の前処理として複雑な単語を限られた語彙集合で分割するアルゴリズムについて向井が話します。感想などはハッシュタグ #misreading か hello@misreading.chat にお寄せください。

• Neural Machine Translation of Rare Words with Subword Units
• [1804.10959] Subword Regularization: Improving Neural Network Translation Models with Multiple Subword Candidates
• google/sentencepiece: Unsupervised text tokenizer for Neural Network-based text generation.
• vocabulary for chromium class names
  • subword examples

 

• WebAssembly Threads ready to try in Chrome 70
  • WebAssembly/threads: Threads and Atomics in WebAssembly

ウェブアプリケーションの JavaScript メモリーリーク検出ツール BLeak ついて向井が話します。感想などはハッシュタグ #misreading か hello@misreading.chat にお寄せください。

• BLeak: Automatically debug memory leaks in web applications
• PLDI ’18 paper

Follow-up

• Python’s New Package Landscape
  • Pipenv ※本編では誤って Pypienv と読んでいますが Pipenv  の間違いです。

マイクロカーネルの上でブラウザを動かすいくつかの研究ついて向井が話します。感想などはハッシュタグ #misreading か hello@misreading.chat にお寄せください。

• Trust and Protection in the Illinois Browser Operating System
• Embassies: Radically Refactoring the Web – Microsoft Research
• L4Android: a generic operating system framework for secure smartphones
  • L4Linux
  • L4Android
• L4 Kernel projects
  • On micro-kernel construction
  • From L3 to seL4 what have we learnt in 20 years of L4 microkernels?
  • seL4: formal verification of an OS kernel

follow-ups

• バスケ on Twitter: “WebView は結構前にDeprecated で次ぐらいで撤去のはず。…
  • UIWebView (deprecated)
• Inside look at modern web browser (part 1) | Web | Google Developers
  • (ちなみに前回のshow notesにもしれっとリンクを貼っていましたがまったく言及していませんでした。すいません）
• Creative Selection
• MinRT by WebAssembly
  • NodeでWebAssembly誰得なのか、みたいなことを話していますが、アーキテクチャやABI等に関係なく再コンパイルなしで使えるという面で好まれることはありうるかもしれません

Chrome オリジナルなプロセス分離ポリシーを突き詰めた研究ついて向井が話します。感想などはハッシュタグ #misreading か hello@misreading.chat にお寄せください。

• Isolating Web Programs in Modern Browser Architectures
  • The Security Architecture of the Chromium Browser
• Chromeのプロセス分離関連
  • Site Isolation
  • Inside look at modern web browser
  • https://twitter.com/kinu/status/1037508916861591552
• Firefox Electrolysis
• Webkit vs Webkit2 API
• 関連研究
  • Tahoma browser: A Safety-Oriented Platform for Web Applications
  • The Multi-Principal OS Construction of the Gazelle Web Browser
• HAL Types  |  Android Open Source Project Treble のプロセスモデルについて
• Android 8.0 Behavior Changes  |  Android Developers WebView のプロセス分離

follow-up

• Kazuyoshi Kato on Twitter: “Rust の場合 out of bounds は実行時に panic, use after free は静的に ownership で防ぐ、はず。ちなみに llvm 経由で各種 san も使えます。たぶんこれは unsafe むけで、レポジトリを持ってる japaric さんは Rust Embedded ワーキンググループのリードです。
• 眼力 玉壱號 on Twitter: “#misreading MSVC に無いのがツライけど、clang-cl 経由で使えるみたいな話を見た様な…