My main project is to create an executable spec of the Intel Architecture but, every now and then, I get to take a broader look at ISA specifications and think about the strengths and weaknesses of other ISA specs: what makes them work well; and what techniques they could borrow from other specifications. Earlier this month, someone asked me for my thoughts on the RISC-V specification and I thought that it would be useful to share what I found out.| alastairreid.github.io
I was long overdue to attend a conference in person: the last conference I attended was POPL 2020. This year’s PLDI was in Orlando, Florida at the height of a hot, humid summer in the largest conference center I have ever seen (we did a lot of walking within the conference center). PLDI was co-located with other conferences including the hardware conference ISCA as part of the Federated Computing Research Conference (FCRC) and I dropped in on a few of the ISCA talks.| alastairreid.github.io
I’ve spent the last couple of years working at Google Research. For the first 5–6 months, I was working in London in an office nestled between King’s Cross station and the iconic St Pancras station. This location was ideal for me because I was still living in Cambridge at the time and it was a very easy journey to either of these stations from Cambridge.| alastairreid.github.io
Last week, I boarded the train to Wadern, Germany (through London, Paris and Saarbrücken) to attend Dagstuhl seminar 23412 on “Formal Methods for Correct Persistent Programming”.| alastairreid.github.io
A couple of weeks ago, I attended PLARCH 2023: a new workshop about the intersection between Programming Languages and Computer Architecture. There was a lot of interest in attending and speaking at the workshop so the program consisted of a lot of short talks with group discussions in between.| alastairreid.github.io
Programming languages provide modules as a way of splitting large programs up into small, separate pieces. Modules enable information hiding that prevents one part of the program from using and becoming dependent on some internal detail of how other parts of the program are implemented. Almost every major language designed in the last 50 years has some form of module system.| alastairreid.github.io
Today I am joining Intel Strategic CAD Labs to work on formal specifications. There’s not much to say so far because I’ve only just started but I think it’s going to be a lot of fun (and a lot of work). I figure that a lot of the first month or two will be spent figuring out what people want to do with formal specifications so, if you think that this will be relevant to you, please get in touch. I am equally interested in uses that are on my list of uses for ISA specifications and uses ...| alastairreid.github.io
Last year, I wrote about the 122 papers that I read in my first year at Google and that I summarize on the RelatedWork site. Over the last 18 months or so, I’ve spent a lot less time doing the one hour train commute between Cambridge and London so I only read 59 papers in the last year and added 188 papers to the backlog of unread papers. You can read my summaries of all the papers, read notes on common themes in the papers, and download BibTeX for all the papers.| alastairreid.github.io
ISA specifications describe the behaviour of a processor: the instructions, memory protection, the privilege mechanisms, debug mechanisms, etc. The traditional form of an ISA specification is as a paper document but, as ISAs have grown, this has become unwieldy. More importantly though, there are more and more potential uses for machine readable, mechanized, executable ISA specifications.| alastairreid.github.io
There are lots of potential uses for machine readable specifications so you would think that every major real world artifact like long-lived hardware and software systems, protocols, languages, etc. would have a formal specification that is used by all teams extending the design, creating new implementations, testing/verifying the system, verifying code that uses the system, doing security analyses or any of the other potential uses. But, in practice, this is usually not true: most real world...| alastairreid.github.io