Blobstore 0.3 draft

This is release 0.3 of the object store; added a bit on the listing invariant, and gave that front page a title.

Looking at this in the context of proof of correctness of the committers

Deployment: the final waterfall

This paper must date from 2001/2002; its an internal doc on deployment, defining the term Continuous Deployment. That was a long time ago

Domain/ OS Design Principles

Domain/OS Design Principles describes the architecture and design of Domain/OS, Apollo's workstation operating system

2005-2006 Bristol Bluetooth dataset

Dataset of discovered bluetooth devices.

This was created from a laptop with a BT dongle, one floor up and 10-15 metres off a street in inner Bristol, not far from Bristol University. Done just with the linux BT daemon set to call a script on every device event, arrival and departure. Needs debouncing, obviously.

Format is Erlang .dat structure: "event", event-type, device ID, timestamp, time_t timestamp

{event,found,"00:12:62:A1:82:81","2005-08-18T20:15:29+01:00",1124392529}.
{event,lost,"00:12:62:A1:82:81","2005-08-18T20:16:14+01:00",1124392574}.

Licence: CC-4.0: Attribution 4.0 International

BTW, there's no code to go with this; nothing particularly interesting, just some basic analysis in erlang just to play with the language. Convert it to CSV and you get to play with it in excel, or Zeppelin standalone

Distributed Programming With System Calls For Interprocess Communications

Programming with System Calls for Interproccess Communication describes the DOMAIN system calls you can use for interprocess communication. Interprocess communication can involve data transfer, event notification and synchronization

Blobstore 0.2: multipart PUT protocol included

This iteration of a TLA+ blobstore specification includes the AWS multipart put operation. That's what I'm using to implement an O(1) committer; having it specified here means that I can work on this spec as the definition of the commit algorithm.

There's one aspect of the multipart operation missing, the bit which declares that the data committed is the ordered sequence of appends. This is tricky-ish as it implies a set-theoretical model of the operation. Because every sequence in TLA+ is really a function 1 |->element1, 2 |-> element2 ... then it can be done using the ordering of the first sequence to define the transformation. It's just beyond my TLA+ ability right now.

A TLA+ specification of a consistent Object Store

This is related to s3guard and other S3A/object store work: I'm trying to defined what an object store should look like, so that we can have a minimal API to work with it.

Surprisingly, there's no example TLA+ spec for this.

Invariants are all based on the "interesting" failures which have surfaced in the past against S3, swift and azure. Some of them may seem obvious, and yes, if the FS were implemented as the simple model in the spec, they would never be false. The fact that they do occasionally fail shows that they have been implemented differently.

TODO

1. Fix the bits that I know are wrong/broken
2. Get defining invariants right.
3. move to some declaration of state over time
4. GET operation to support a length/offset

TLA+ YARN registry specification in sync with YARN-913 patch-002

This is a TLA+ specification covering patch 002 of the registry —with the purge() operation to delete entries as their container/app attempt or app expire.

I don't think it's correct yet ... that logic about action queues (borrowed from the co-ordination spec) may be over complicating things. Or it may be needed but I just don't understand that much of TLA+ yet

Publishing of 1989 final year project, "The Ultimate RISC"

The Ultimate RISC

formal specification and implementation of a single instruction microprocessor.

Steve Loughran, June 1989.

Clearly dated in its naive optimism about the application of formal methods to hardware design, my final year undergraduate project covered the specification and then implementation of one of the few microprocessors to be so formally specified.

At the time of writing I believe the others were

1. The Viper Microprocessor
2. The floating point unit of the T800 Transputer

ALUs and FPUs are more tractable to formal specification as the operations themselves are straightforward to define: addition, division, shifting, etc. For my work, it was possible to actually execute that bit of the design in Standard ML, even if Kevin Mitchell &c hadn't got round to implementing ints >32 bits. Of course, in a pre-test-centric world the execution of those bits was limited, though even in a test-first era, the test space of an ALU is too vast for coverage -hence the advantage of formality.

The full specification has include temporal logic as operations take cycles; the output at t(n+1) depends on the input att(n). Once you add feedback loops (e.g. carry bits), then life gets even more complex.; the state at t(n+2) also depends on the input att(n)... Hence: temporal reasoning.

Implementation wise, 74F- series TTL parts with a simple programmable part for the state machine of the CPU itself, again derived (manually) from that specification.

What actually caught me out, I recall, were

• Sub-nS glitches on the wire, triggering state transitions to early —glitches only observable once I (eventually) cranked the logic analyser up to full resolution.
• The +ve power rail dropping below the 5V needed for the TTL parts to work properly, something that happened very subtly as more parts of the system were implemented. The failure modes were non obvious, even if the solution, once discovered was.
• Me frying some part. This is where hardware differs from SCM-managed applications. If you are a competent developer, you never actually fry one of your source code modules, you just break a test and then roll back.

My conclusions from that actual building experience were

1. Hardware is analog, no matter how much it pretends to be digital —and it is that difference which gets you no matter how well you try and specify it at the digital level.
2. I'm too good at breaking things to be a hardware developer.

Looking back at the code (p142+), it's vaguely familiar, but I'm certainly not competent enough in SML to code it right now. I also note a couple of references to Church's iota operator. I have no idea or memory what that is —though I'm confident it is related-to or part-of the Lambda calculus. Or I just made it up to sound like I knew what I was talking about.

Acknowlegements

• Nigel Topham, supervisor
• Prof Mike Fourman, for the specification language and help getting it to work.