Flandre’s lecture on QED

Hey, I don’t think I’ve seen you before. I’m Remilia’s little sister, Flandre Scarlet. It’s been a while since Remi sent anyone down to the basement for me to play with.

You look scared. Remi must have told you that I’ve been sealed here for over 400 years because I’m unstable and destructive. That’s not true at all, trust me. Do I look like an unstable and destructive person to you? I’m not going to hurt you. I just want to play with you.

By “play” I mean “discuss concurrent programming concepts”. Yeah, being stuck down here in the basement with nothing but books and computers to play with has kind of made me an expert programmer.

Today I’ll tell you about this special system I developed called QED. It’s used to verify that concurrent programs work the way they should. In the outside world, a team of Turkish programmers developed this in a couple of years. My version of QED isn’t as robust as theirs, and it’s taken me over 10 years to develop. I blame hardware failure. The computers Sakuya sends down here for me to work with never last for very long before they break. It’s really annoying.

So, computer processors aren’t getting any faster these days, but programs are. How do they manage this? By using multiple processors working in parallel. If you have ten problems to solve, or ten processes to run, you can give five to one processor and five to the other, and get them done in half the time it would take a single processor.

These programs are called “concurrent programs” because they consist of multiple processes running at the same time. The problems arise when the multiple processes are working on the same variables. Take the example above, which is the simplest possible concurrent program I can think of. Two separate processes take a number and add one to it. When both processes are done, you want the number to be two greater than what you started with.

If the second process waits until the first one is done before taking its turn, the program behaves properly. However, if the second process doesn’t wait, and gets the value to add before the first process has added one to it, the number only increases by one, not two, once both processes are finished.

This is the main problem of concurrent programs. To make things worse, because the interleaving of instructions between the concurrent processes is different each time, the program sometimes behaves correctly, making the problems harder to detect. With a simple program such as the above, it’s pretty easy to see the cases that cause errors, but the difficulty of finding errors increases greatly as the program becomes more complex.

To fix problems like these, we implement “locks” on variables. In order for a process to read or change a variable, it must first acquire a lock for that variable. When it’s done with its operations, it releases the lock. While a given process holds a lock, no other process can read or change that variable (although locks with less restrictions do exist).

With the locks in place, whichever process acquires the lock first gets to add one to the variable, and the other process has to wait for the first process to release the lock before it can read the value of the variable and add one to it. Admittedly this cancels the benefit of having two processes working at the same time, but it’s better than causing errors.

Even with locks though, such a program can be hard to verify (that is, to say that it is guaranteed to do what you expect it to, in this case to increase a number by two). Verifying programs is done with an invariant, a condition that you want to be true at any point in the program, shown above in red.

Can’t read the red text? Well, I can’t either.

And that’s just the first two of 12 statements OR’d together, essentially describing every possible state of the program. Does it seem needlessly complex? It does to me, and this is the simplest possible concurrent program.

That’s where we bring in QED. QED is an acronym for the Latin phrase “quod erat demonstrandum”, which literally means “which was to be demonstrated”, and is used at the end of a mathematical proof to show that a theorem is true. We borrow the term here to prove that a concurrent program does what it’s supposed to.

QED breaks a program down into its component atoms, or pieces that are considered to run as a single action without any other actions taking place at the same time. Have you ever tried breaking something down into its component atoms? It can take hours of smashing, and there’s so much collateral damage that Sakuya has to stop time to clean up the mess. But it’s a lot of fun.

Now, where was I?

Assuming that the locks work correctly, we have two atoms, each of which adds one to a number.

Notice how much simpler the invariant has become.

And we can simplify further. QED can determine which processes need to execute on their own, and which processes can be executed at the same time as others. QED classifies each atom as “left-moving” (can happen as early in the program as possible and not cause an error) or “right-moving” (can happen as late in the program as possible and not cause an error). In the above example, where two atoms both add one to a number, both are left-moving and right-moving, meaning the order in which they execute doesn’t matter, as long as one process doesn’t execute while the other is executing.

By using locks (as described above) and assertions (which terminate the program if a variable does not match an expected value) programs can be made so that every time they run, they either operate properly or terminate, and never give the incorrect output. To summarize,

Wow, that’s it! You actually got to the end of my lecture on QED! Only Reimu and Marisa have gotten to the end of QED before today. Reimu… well, Reimu is hax, so she can get to the end of anything. And Marisa… I must have been too… star-struck to care whether she was actually listening.

I miss Marisa. I wish she would come back some day and play with me again. Wait, come to think of it, Patchouli mentioned Marisa dropping by the other day. Does that mean Marisa came by to see Patchouli and not me? And the look in Patchouli’s eyes when she told me about it… I swear, if that purple beansprout is thinking of putting the moves on my Marisa, I swear, I’ll… I’ll…

Oh, looks like we have another equipment failure. At least it was only the monitor. Computing technology is so unreliable. How did people in the outside world ever come to depend on computers on a daily basis?

Hey, where are you going? Don’t you want to play some more? Don’t run away!

They got away…

I’m all alone again…

(Information taken from this lecture.)

3 Responses to “Flandre’s lecture on QED”

  1. Sixten says:

    @Samukun: I played it. Short and no choices, but good stuff. Makes me want to make a Toho VN of my own (Cirno-based, of course).

  2. Zeroblade says:

    If only those lectures you were taking were a regular thing, then we could have all these awesome posts all the time!

Leave a Reply