[article][distributed]
We present a formal, machine checked TLA+ safety proof of MongoRaftReconfig, a distributed dynamic reconfiguration protocol. MongoRaftReconfig was designed for and imple- mented in MongoDB, a distributed database whose replica- tion protocol is derived from the Raft consensus algorithm. We present an inductive invariant for MongoRaftReconfig that is formalized in TLA+ and formally proved using the TLA+ proof system (TLAPS). We also present a formal TLAPS proof of two key safety properties of MongoRaftReconfig, Leader- Completeness and StateMachineSafety. To our knowledge, these are the first machine checked inductive invariant and safety proof of a dynamic reconfiguration protocol for a Raft based replication system.
https://will62794.github.io/assets/papers/cpp22-formal-verification-reconfig.pdf
We present a formal, machine checked TLA+ safety proof of MongoRaftReconfig, a distributed dynamic reconfiguration protocol. MongoRaftReconfig was designed for and imple- mented in MongoDB, a distributed database whose replica- tion protocol is derived from the Raft consensus algorithm. We present an inductive invariant for MongoRaftReconfig that is formalized in TLA+ and formally proved using the TLA+ proof system (TLAPS). We also present a formal TLAPS proof of two key safety properties of MongoRaftReconfig, Leader- Completeness and StateMachineSafety. To our knowledge, these are the first machine checked inductive invariant and safety proof of a dynamic reconfiguration protocol for a Raft based replication system.
https://will62794.github.io/assets/papers/cpp22-formal-verification-reconfig.pdf
[article]
Many organizations are shifting to a data management paradigm called the “Lakehouse,” which implements the functionality of struc- tured data warehouses on top of unstructured data lakes. This presents new challenges for query execution engines. The execu- tion engine needs to provide good performance on the raw un- curated datasets that are ubiquitous in data lakes, and excellent performance on structured data stored in popular columnar file formats like Apache Parquet. Toward these goals, we present Pho- ton, a vectorized query engine for Lakehouse environments that we developed at Databricks. Photon can outperform existing cloud data warehouses in SQL workloads, but implements a more general exe- cution framework that enables efficient processing of raw data and also enables Photon to support the Apache Spark API. We discuss the design choices we made in Photon (e.g., vectorization vs. code generation) and describe its integration with our existing SQL and Apache Spark runtimes, its task model, and its memory manager. Photon has accelerated some customer workloads by over 10× and has recently allowed Databricks to set a new audited performance record for the official 100TB TPC-DS benchmark.
https://www-cs.stanford.edu/~matei/papers/2022/sigmod_photon.pdf
Many organizations are shifting to a data management paradigm called the “Lakehouse,” which implements the functionality of struc- tured data warehouses on top of unstructured data lakes. This presents new challenges for query execution engines. The execu- tion engine needs to provide good performance on the raw un- curated datasets that are ubiquitous in data lakes, and excellent performance on structured data stored in popular columnar file formats like Apache Parquet. Toward these goals, we present Pho- ton, a vectorized query engine for Lakehouse environments that we developed at Databricks. Photon can outperform existing cloud data warehouses in SQL workloads, but implements a more general exe- cution framework that enables efficient processing of raw data and also enables Photon to support the Apache Spark API. We discuss the design choices we made in Photon (e.g., vectorization vs. code generation) and describe its integration with our existing SQL and Apache Spark runtimes, its task model, and its memory manager. Photon has accelerated some customer workloads by over 10× and has recently allowed Databricks to set a new audited performance record for the official 100TB TPC-DS benchmark.
https://www-cs.stanford.edu/~matei/papers/2022/sigmod_photon.pdf
[article]
https://github.blog/2022-06-29-improve-git-monorepo-performance-with-a-file-system-monitor/
https://github.blog/2022-06-29-improve-git-monorepo-performance-with-a-file-system-monitor/
The GitHub Blog
Improve Git monorepo performance with a file system monitor
Monorepo performance can suffer due to the sheer number of files in your working directory. Git’s new builtin file system monitor makes it easy to speed up monorepo performance.
[article][interview]
https://4dayweek.medium.com/netflix-interview-process-questions-best-practices-2022-1fdca3bb36c6
https://4dayweek.medium.com/netflix-interview-process-questions-best-practices-2022-1fdca3bb36c6
Medium
Netflix interview process, questions & best practices (2022)
Netflix is part of the FAANG (Facebook, Amazon, Apple, and Google) group of companies. Apart from these companies being part of the NASDAQ, they are also known for being even harder to get into than…
[article][sharding]
https://blog.twitter.com/engineering/en_us/topics/infrastructure/2021/sharding-simplification-and-twitters-ads-serving-platform
https://blog.twitter.com/engineering/en_us/topics/infrastructure/2021/sharding-simplification-and-twitters-ads-serving-platform
X
Sharding, simplification, and Twitter’s ads serving platform
Learn how Shardlib, a new sharding library at Twitter simplifies the management of sharded ads services and enables dynamic resharding of these services without redeploying their clients.
👍2
[course][math]
https://www.jonkrohn.com/posts/2021/5/9/linear-algebra-for-machine-learning-complete-math-course-on-youtube
https://www.jonkrohn.com/posts/2021/5/9/linear-algebra-for-machine-learning-complete-math-course-on-youtube
Jon Krohn
Linear Algebra for Machine Learning: Complete Math Course on YouTube — Jon Krohn
There are 48 YouTube videos in my Linear Algebra for Machine Learning course, each of which is detailed in this blog post.
[ml][links]
Good friend of mine just passed Google ML certification. He prepared some materials he found useful during that journey:
https://iron-football-358.notion.site/GCP-ML-Engineer-notes-d13654b2ef0749808ea525370cc24071
Good friend of mine just passed Google ML certification. He prepared some materials he found useful during that journey:
https://iron-football-358.notion.site/GCP-ML-Engineer-notes-d13654b2ef0749808ea525370cc24071
Egor's Notion on Notion
GCP ML Engineer notes
Note, that this collection of links and topics does not cover the ML/DL part of the exam, in order to prepare for that I’d recommend reading through the book “Geron Aurelien. Hands-On Machine Learning with Scikit-Learn, Keras, and TensorFlow” and doing some…
🔥3