Welcome to Waqas' blog
LinkedIn Queens is a puzzle played on an n × n grid with the following rules: The grid is divided into n colored regions. Each row, column, and colored region must contain exactly one queen. No two queens may be adjacent, including diagonally. However, diagonals at a distance are allowed. In this post, we look for all solutions, not just one, using a Python-based SAT solver and Spin, a model…
When I enjoy a book, I often look for other work by the same author. While reading a book by Ben-Ari, I looked up his other writing and came across a paper on the Santa Claus concurrency puzzle 1 . The puzzle is stated as follows: Santa Claus sleeps at the North Pole until awakened by either all nine reindeer or a group of three out of ten elves. He performs one of two indivisible actions: If…
AWS published a post-mortem about a recent outage [1]. Big systems like theirs are complex, and when you operate at that scale, things sometimes go wrong. Still, AWS has an impressive record of reliability. The post-mortem mentioned a race condition, which caught my eye. I don’t know all the details of AWS’s internal setup, but using the information in the post-mortem and a few assumptions, we can…
I came across a fascinating and surprising aspect of a seemingly simple concurrent program when run on a model checker. Consider this: If we run P and Q concurrently with ‘n’ initialized to zero, what could be the lowest value of ‘n’ when the two processes finish executing their statements on a model checker? Can a model checker also help us find the extreme interleaving that produces this lowest…
Concurrent programming is hard. Mentally enumerating all the possible states that complex concurrent code might go through is far from easy. Visualizing concurrency can make it easier to understand how these programs operate, especially for those just beginning to learn about concurrency. Such visualizations might not always be effective for larger or more complex systems. But even with complex…
PROMELA is a language used to write models that can be validated with the SPIN model checker. To facilitate data exchange between processes, PROMELA provides the concept of channels. These channels are essential when creating a model where processes need to communicate and share data. Channels allow two processes to exchange information. One process can send data through a channel, and another…
The PROMELA language is used to write models in the SPIN model checker. PROMELA’s syntax is similar to C, but its control statements are inspired by a formalism called “guarded commands,” invented by E.W. Dijkstra, which is particularly well-suited for handling nondeterminism. Let’s start by examining the if statement in PROMELA. It begins with the reserved word “if” and ends with “fi.” Within it,…
Gentzen system, created by German mathematician Gerhard Gentzen, is a deductive system which can be used to prove propositional formulas. I recently learned about it while I was reading Ben-Ari’s fantastic book on mathematical logic [1] and I like its simplicity. Should we care about the Gentzen system? Let’s say you’re a programmer, why should you care about logic or mathematical reasoning? I…