csgordon

The Programming Systems Seminar is a seminar for discussing and presenting research in "programming systems," broadly construed, which includes at least programming languages, software engineering, compilers, and any work relevant to improving the design and construction of software.

The goals for the seminar are:

• To stay up to date on developments in this (broad) area
• To build some community among researchers (faculty and students) in related areas
• To give students additional practice presenting research ideas, including presenting ideas they are more familiar with to those not in their own immediate research area

csgordon

Installing OpenBSD 7.3-current on a VisionFive2

Here are some concise instructions for getting OpenBSD 7.3-current running on a StarFive VisionFive 2 (v1.3B, though from other reports referenced below, it sounds like the v1.2 boards can also be made to work).

You will need:

• An SD card of at least 1GB
• An eMMC module attached to the board (though see below for a variation that should work to install directly to sd card)
• Internet access
• A USB TTL serial adapter that supports 3.3V (some of these support multiple voltages, but if yours only supports other voltages and not 3.3 it will either not work or damage your board!)

csgordon

We're no strangers to love
You know the rules and so do I (do I)
A full commitment's what I'm thinking of
You wouldn't get this from any other guy
I just wanna tell you how I'm feeling
Gotta make you understand
Never gonna give you up
Never gonna let you down
Never gonna run around and desert you
Never gonna make you cry

csgordon

#!/bin/sh
# Secret is the -r option to cvt. The rest of these settings are based on that modeline.
# Also important, for NVidia cards, this only works with the Noveau driver, not the proprietary one.
# cvt -r 2560 1440
xrandr --newmode "2560x1440R"  241.50  2560 2608 2640 2720  1440 1443 1448 1481 +hsync -vsync
xrandr --addmode DP-1 "2560x1440R"
xrandr --output DP-1 --mode 2560x1440R --rate 60

csgordon

Getting Help

Getting help with FreeBSD has been... interesting.

The best place to start is often the FreeBSD forums, where the question you may have has very often been answered in full. But this comes with some important caveats:

• The forums explicitly state that if you're using a derivative (like GhostBSD) then the forum rules say to just not post there. This is on one hand understandable: derivatives in general can make wild changes (I've been around long enough to remember early Ubuntu users trying to get help from long-time Debian users.... even early Ubuntu had made major changes to the point where Debian users genuinely couldn't help). And certainly there are some FreeBSD derivatives that have made major changes, like helloSystem and ravynOS, not to mention whatever sourcery NomadBSD has done to filesystem mounting. On the other hand, GhostBSD seems (famous last words) to have made rather minimal changes

csgordon

FROM ubuntu:focal-20200729

# Core stuff
ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update
# Apparently installing tzdata here explicitly avoids an interactive dialog later
RUN apt-get install -y apt-utils tzdata
RUN ln -sf /usr/share/zoneinfo/US/Eastern /etc/localtime
RUN dpkg-reconfigure -f noninteractive tzdata
#RUN ntpd -gq

csgordon

I've been running Linux in Hyper-V for some time, as an alternative to remotely connecting or dual-booting. A perpetual problem with this, however, is that Hyper-V's hyperv_fb driver only supports monitor resolutions up to 1600x1200, and doesn't support resizing. (Microsoft has guest extensions, but they are gradually maintained for fewer and fewer variants of Linux; currently it appears only RHEL is actively maintained, with the latest Ubuntu release supporting 18.04. It is now 2020.)

I've tried a number of different approaches to connecting remotely to a Hyper-V machine over the years, and most break after some period of time. I have a relatively stable solution for connecting to a Docker container with RDP, but if I want to run programs using lots of memory, I don't necessarily want to dedicate that much memory to the main Docker host VM.

The following short script is based on instructions I found for making it possible to SSH

csgordon

Thank you for your reviews. After a shorter general response, there are point-by-point responses for those inclined to read them.

As far as motivation (Reviewer A): there are currently a range of interesting program analyses formulated as sequential effect systems. Currently, none of them can handle control flow more complicated than while loops or simple recursion. Exceptions and generators, which are now widespread, have never been addressed in any sequential effect system. While there is perhaps a case to be made that delimited continuations might be "more" than we should address directly (Reviewer B), it seems that growing interest in algebraic effects (tunneling algebraic effects are essentially tagged delimited continuations) and the impending addition of explicit delimited

csgordon

/*
 * Sample code for the AGERE 2019 paper "Modal Assertions for Actor Correctness" by Colin S. Gordon, DOI 10.1145/3358499.3361221.
  * Note that at the time of this writing, there is an issue (https://github.com/dafny-lang/dafny/issues/359) where this file only verifies from the command line (modulo complains about missing implementations of abstract methods).  Currently, verifying this via the Dafny Visual Studio Code plugin runs into trouble with the higher-order predicates.

 * Last checked with a local build of Dafny commit 8f141e9d05b2dba9de4ba997040df6166c2d168c and Boogie commit bc49937e7ee88e931bbe2dbf779a42612731a8fd
 */

module ActorCore {
    class {:extern} ActorRef<Ms> {}
    predicate {:extern} at<T,Ms>(i: ActorRef<Ms>, p:(T ~> bool))

csgordon

module ActorCore {
    class {:extern} ActorRef<Ms> {}
    predicate {:extern} at<T,Ms>(i: ActorRef<Ms>, p:(T ~> bool))
    /* at[i](_) is a modality */
    lemma atImpl<T,M>(c:ActorRef<M>, P:T~>bool, Q:T~>bool)
        requires forall x:T :: P.requires(x) ==> Q.requires(x)
        requires forall x:T :: P.requires(x) ==> P(x) ==> Q(x)
        ensures at(c, P) ==> at(c, Q)
    /* When using the above, Dafny sometimes doesn't notice the precondition holds;
    this variant forces it to look for it. */