Update 2023-12-11-A DSL for Metastability.md

content/blog/2023-12-11-A DSL for Metastability.md

@@ -207,7 +207,7 @@ In a nutshell, this is what happens:
 4. There is a special message of the type "update", that can be injected anytime by the environment. This message abruptly takes the agent to the listening state, no matter the value of the timers.
 
 Metastability in this example happens when a triggering update message is injected into one of the agents, possibly by a network operator playing the role of the environment.
-As a result, all of the agents are eventually synchronized, meaning that they send their routing messages at axactly the same time.
+As a result, all of the agents are eventually synchronized, meaning that they send their routing messages at exactly the same time.
 This is undesired behavior in a realistic network, as it introduces bursts of packets periodically.
 As an analogy to the retry storm example, the self-sustaining loop here is the synchronous firing of routing messages.
 
@@ -234,4 +234,4 @@ The following list, by no means exhaustive, sheds light on some of the noteworth
 1. The ownership model of Rust, in tandem with the borrow-checker, is a totally new way of thinking about code for me. Things that are pretty straightforward in other languages become complicated. This problem is exacerbated by the fact that I find it convenient to pack stuff together into a struct, and it is not trivial to me at all how to use a struct's methods on itself with a careful observation of ownership, specially in recursive calls.
 2. As I mentioned earlier, I have decided to make the DSL look like NetKAT. My hunch for this was that the general story in our setting looks very similar to the one studied by NetKAT: requests (packets) travelling around, and getting processed by agents (routers) based on their type (port, switch, etc). However, the semantics are currently drastically different. The important abstraction in NetKAT is a packet, and the semantics revolves around a packet: the network is a mapping of a packet to a set of packets. In our DSL, in contrast, the semantics is much more similar to the classic small-step semantics of, say, IMP, where you have a state (or a store), and you apply some operations on it. My hope was to be able to use something similar to the equational inference system baked into NetKAT, via Kleene algebras, to study metastability. I have not yet seen a clear connection.
 3. On the long run, one would hope to have a performant interpreter, i.e., one that can interpret large systems in a short span of time. The crux of the difficulty lies in parallelizing the execution in the right way. While there are straightforward ways of attempting this, I have not yet found a good way of doing it.
-4. The previous point is exacerbated by the fact that one would also like to have a model-checker that would use the interpreter. Ideally, the model-checker would receive a given system and produce a trace "ending" in a bad self-sustaining loop caused by a trigger. Following the maxim "immature optimization is the root of all evil", I have not spent much time thinking about this yet, but I am expecting some serious issues down the road.
+4. The previous point is exacerbated by the fact that one would also like to have a model-checker that would use the interpreter. Ideally, the model-checker would receive a given system and produce a trace "ending" in a bad self-sustaining loop caused by a trigger. Following the maxim "immature optimization is the root of all evil", I have not spent much time thinking about this yet, but I am expecting some serious issues down the road.