Professor

Christopher A. Stone

Email: | `stone@cs.hmc.edu` |

Phone: | (909) 607-8975 |

Admin: | (909) 621-8225 |

Fax: | (909) 621-8465 |

Office: | Olin B157 |

Teaching

During Fall 2022 I am teaching two sections of a brand-new course, CS 181AF: Advanced Data Structures.

I am also advising a Clinic senior capstone project.

Research, present and past

While proving mathematical theorems is hard and can require clever
insights, checking that a well-written proof is free of errors (that
each step follows from the previous ones) is a task well-suited to
computers. The most successful proof checkers are based on
*Type Theory*, which blurs the lines between mathematical proofs
and executable programs. For efficiency (and decidability) reasons,
these systems usually distinguish between
*definitional* equality (two ways of writing the obviously the same
thing, like \(3+1 = 4\) and
*propositional* equality (equalities that need a justification
before the computer will accept them, like citing the Pythagorean
Theorem to get \(a^2 + b^2 = c^2 \).

The dividing line is not always clear. For example, if
`rev`

is a function for reversing lists, then obviously
`rev(rev(l)) == l`

; are these just two ways of describing the
same list, or is simplifying
`rev(rev(l))`

to `l`

a step worth noting?

Most computer-assisted proof systems have some definition of
definitional equality built in; all other equalities require proof.
Definitional equality is kept minimal, which can lead to awkwardness.
For example, commonly a list of length `(0+n)`

is also a list
of length `n`

, because `0+n == n`

is considered to
hold by definition. But to treat a list of length `n+0`

as a
list of length `n`

requires an explicit justification
(because `n+0 == n`

is a propositional equality that requires
proof).

Prof. Andrej Bauer and I are looking at more flexible systems where definitional equality can be extended as needed (e.g., to allow 0+n == 0 and n+0 == 0 as built-in facts), in the context of a particular system called Homotopy Type Theory (HoTT). The cost of this extra flexibility (and the reason why most systems limit definitional equality) is that proof checking becomes an undecidable problem, impossible for a computer to solve in general! But by letting the proof author supply “hints” in a low-overhead way, we can avoid the general undecidability problems and successfully check all the specific cases we would care about.

Errors in software become more expensive and dangerous each year. Testing is helpful, but proofs are the only way to truly guarantee that an algorithm is correct, or that a cryptographic protocol is secure, or that a programming language is safe.

Unfortunately, it’s hard to get all the details of a big proof right; even careful reasoners make mistakes, and even careful readers miss them. Automation seems a natural solution, and there exist “proof assistant” systems to help people construct and verify proofs, using special-purpose computer languages. In the end, though, we have a proof that we are sure is correct but that is almost unreadable if you’re not a computer!

I want a system that can verify proofs that were written for humans to read and understand, the kind of proofs you see in textbooks and research papers. Essentially, I want to go beyond spell-checking and grammar-checking to logic-checking.

Multicore processors are ubiquitous in desktops, laptops, and even cell phones have multicore processors, yet they are still too hard to program. The most common approach involves “locks,” which are tricky and error-prone (not enough locks → race conditions; too many or out of order → deadlock). Newer techniques like Transactional Memory can be awkward to use.

Observationally Cooperative Multithreading (OCM) is an approach to parallel programming that I have been investigating with Professor Melissa O’Neill and an impressive series of 33 undergraduates over the past seven years.

We start with classical Cooperative Multithreading (CM), where only one thread runs at a time, and each thread gets the whole machine to itself until it explicitly yields control to the next. CM is a very convenient programming model; if threads are only interrupted when they choose to be, then locks and the problems that go with them can largely be avoided.

OCM lets us write programmer-friendly CM code, yet still advantage of multiple processors. Code runs “as if” one thread were running at a time. But when two threads are independent, an OCM system can run them simultaneously to get the same answer, but faster!

To learn more about the OCM model, I recommend starting with this (unpublished) introduction to Observationally Cooperative Multithreading. Our best implementation is described in the TRANSACT 2015 paper Making Impractical Implementations Practical: Observationally Cooperative Multithreading Using HLE.

Plus: Lists are easy; what does it mean to “code up” a smooth manifold, or the mathematical set ℝ?

The RZ system translates specifications for mathematical structures into specifications for code. It answers questions like, “What would a programmer need to implement in order to get a complete and correct implementation of the mathematical (“real”) real numbers [ or of a compact metric space, or a space of smooth functions, …]?”

From an educational perspective, RZ also provides explanations (in terms
a programmer can understand) of the non-classical distinctions that
arise in constructive mathematics. For example, it can be used to
explain the difference between a finite set and a set that is not
infinite, and why there a `size()`

function only for the former.

You can look a list of selected papers and talks or my full CV.

Code and other artifacts

I’m glad you asked! I put together an implementation as an offshoot of the OCM research project.

Octet locks are interesting for concurrent programming because threads aren’t required to unlock when they’re done; this can be a big speed advantage for resources that are accessed mostly by a single thread. Further, Octet locks can be acquired in any order without fear of deadlock (though while acquiring one lock you might lose others).