Skip to content

Instantly share code, notes, and snippets.

Martin Kleppmann ept

Block or report user

Report or block ept

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View Consensus_Demo.thy
theory
Consensus_Demo
imports
Network
begin
datatype 'val msg
= Propose 'val
| Accept 'val
@ept
ept / gist:4475995
Last active May 19, 2019
Syntax highlighting code for PowerPoint (Mac OS)
View gist:4475995

How to add syntax-highlighted code to PowerPoint slides (Mac OS)

  1. pygmentize -f rtf FILE | pbcopy
  2. Paste into TextEdit (in rich text mode: Format → Make Rich Text before pasting), and copy to clipboard again.
  3. In PowerPoint, Edit → Paste Special… → Styled Text.

(Pasting RTF directly into PowerPoint doesn't work correctly, at least with PowerPoint 2008 — it extends colour spans longer than it should, and sometimes removes line breaks. Going via TextEdit seems to solve the problem.)

@ept
ept / TestUnionEvolution.java
Created Dec 14, 2015
Adding a new branch to an Avro union
View TestUnionEvolution.java
import java.io.ByteArrayOutputStream;
import java.io.IOException;
import org.apache.avro.Schema;
import org.apache.avro.generic.GenericData;
import org.apache.avro.generic.GenericDatumReader;
import org.apache.avro.generic.GenericDatumWriter;
import org.apache.avro.generic.GenericRecordBuilder;
import org.apache.avro.io.BinaryDecoder;
import org.apache.avro.io.BinaryEncoder;
import org.apache.avro.io.DatumReader;
@ept
ept / _summary.md
Last active Dec 7, 2018
Notes on Mark Hayter's stylus talk
View _summary.md

Stylus input and the benefits of a standard

Notes from a talk by Mark Hayter

Mark Hayter is Senior Engineering Director in the Chrome OS Hardware team at Google, and currently a visitor from industry with the Computer Architecture team in the Computer Lab.

  • 1990s: Apple Newton, Palm Pilot used graffiti input (one letter at a time, stylised), Lectrice
  • 2000s: Microsoft Tablet PC
View coed-ethics.md

Notes from Coed:Ethics conference, London, 13 July 2018

Cori Crider - "When data kills" / Weaponised AI

  • Imam Salem bin Ali Jaber preached in Yemen against Islamic extremism; guest at a wedding of relative; hit by a US Hellfire missile fired from a drone. Relative Faisal made contact with Cori, went to Washington DC. No explanation ever made by government (although compensation was paid).
  • Decision-making process behind the attack not known exactly. But there is significant evidence that such attacks serve to further radicalise people; attack results in ~3x more new recruits than extremists killed by attack.
  • Most drone attacks are not on named individuals, but rather "signature strikes" — a euphemism for killing people the military doesn't even know, but who match a certain behavioural pattern (perhaps based on metadata — Hayden: "we kill people based on metadata"
  • Skynet (known through Snowden relevations): use machine learning to try to find courier
@ept
ept / dataloss.rb
Created Jan 24, 2017
Calculate the probability of losing all replicas of a partition in a cluster
View dataloss.rb
# Parameters:
prob_nodefail = 0.001 # Probability of a single node failing
replication_factor = 3 # Number of copies of each partition (r)
partitions_per_node = 256 # Number of partitions per node
max_nodes = 10000 # Maximum number of nodes to consider
# (n - r)! / n! == r! / (n choose r)
# Intuitively: the fraction of the n! possible permutations of n nodes that
# results in the replicas of one particular partition to be mapped to three
# particular nodes, in a particular order.
View AvroTest.java
import java.io.ByteArrayOutputStream;
import java.io.IOException;
import org.apache.avro.Schema;
import org.apache.avro.generic.GenericData;
import org.apache.avro.generic.GenericDatumReader;
import org.apache.avro.generic.GenericDatumWriter;
import org.apache.avro.generic.GenericRecordBuilder;
import org.apache.avro.io.BinaryDecoder;
import org.apache.avro.io.BinaryEncoder;
import org.apache.avro.io.DecoderFactory;
View trve-2016-11.md

TRVE Data update — November 2016

This update was sent by email to the TRVE Data mailing list on 1 December 2016. Please subscribe to the mailing list or follow us on Twitter for future updates.

Hello TRVE Data supporters,

Here's an update on what we've been doing in November.

  • Stephan has made great progress on understanding Tor network traffic. He is now able to trace almost all data transfer through the various layers — application data, Tor circuits, calls to the OpenSSL library, down to actual network packets — and thus analyse each packet to determine why it was sent or received. This is especially important when using Tor on mobile devices, since every network packet uses battery energy and costs money (depending on your data plan). By labelling network packets, we can compare protocol changes to
View update.md

TRVE Data update — Sept/Oct 2016

Hello TRVE Data supporters,

Sorry for the lack of an update last month. Here's what we've been up to in September and October.

Diana and Martin presented an introduction to end-to-end encryption protocols at the Strange Loop conference in St Louis, and repeated the talk in Cambridge. We illustrated network communication and man-in-the-middle attacks by passing pieces of cardboard back and forth on the stage -- a visualisation that went down well with the audience.

Alastair and Martin have been working together with Dominic Mulligan and Victor Gomes, also researchers in Cambridge, on formalising our JSON CRDT definition using the Isabelle proof assistant. We are converting the hand-written convergence proof in our paper into a machine-checkable proof,

View trve-2016-05.md

TRVE DATA monthly update: May 2016

Hi everyone, the month of May has flown by, and it's time for our second monthly update for the TRVE DATA project.

In case you missed it, last month's update is here: https://gist.github.com/ept/627b4f102a0a036cee0b941a8b8e31c2

Here's what's new in May:

  • Stephan has been doing some measurements to determine the overhead of running a Tor hidden service on a smartphone, which could be used to exchange messages between devices directly in a privacy-preserving way. He found that just keeping the hidden service alive produces several hundreds of megabytes per month in traffic. To a large extent this seems to be caused by regularly downloading information about the status of all Tor relays. As this amount of overhead is not acceptable for many users with a limited data allowance, an open question is whether we can reduce the amount of data that needs to be downloaded, and what the trade-offs are.
You can’t perform that action at this time.