During the last 20 days, I haven’t written in this blog. There are reasons, although I have to admit I did not work a lot during those days.
The day after my last post, my mom arrived from Germany and spent nearly two weeks here. Fortunately, the weather was nice, not too hot and only one day of rain. We had a lot to talk about, and if you know anything about my personal life, you can imagine that this was sometimes straining. On the other hand, I enjoyed her stay more than ever this time: In the past, I’ve always had the feeling that I didn’t spend enough time with her because I still had to grade or work on my projects. This time, her visit fell into the weird period when I had mostly finished writing my thesis, but I couldn’t defend yet. So we used the time for several long walks and discussions, about important things as well as trivial things. I miss her, and I can’t wait for her to be back. She will be; I guarantee it.
As already stated, I couldn’t defend my Master’s thesis in May as planned; it was too late for graduating in May anyway, but only by a couple of weeks. Because of that, I’m not too disappointed: It would have been nice, but it wasn’t really necessary. I sent out review copies of my thesis, but unfortunately, so far I haven’t got a lot of feedback.
The only person that provided a detailed review was Justin. Thanks again, Justin, you have been a great help and wonderful friend. When talking to you about my thesis and your comments, I have realized again what an extraordinary person you are: Not only did you comment on what I had written down, you also asked questions about what I still have to do. Even though it is my task to figure things out and answer some of the difficult questions, you have gone beyond what I asked of you as a favor and have spent your time and have thought about what future problems I will face. Again, I can only marvel at your curiosity, intuition and energy. Thanks. I’ll try to repay the favors some time.
Justin helped me with two problems: First, while reading some type theory books I had loaned him, he asked a few questions about the Bottom type. In trying to answer these questions, I have realized I have a mistake in my thesis; not a major one, but I’m stating something that isn’t correct. Second, Justin helped me with the idea of schedule generation, a topic that I’ll still have to work on.
When Justin returned the review copy of my thesis, he asked questions along the lines of “Are there any values of type Bottom?”, “What does returning Bottom mean?”, and “How does returning Bottom differ from returning Unit?”. After trying to get my head straight for a few minutes, I finally explained that Bottom is a type that is a subtype of any other type. Whatever type you give me, Bottom is a subtype of it. That also means that if there were a value of type Bottom, then its type could be promoted to any other type. This is similar but more general than the relationship between the Java classes String and Object: Any value of class String can also be promoted to type Object.
Upon closer analysis, the fact that a value of type Bottom can be promoted to any other type is also the reason why there is no value of type Bottom. If that value existed, then its type could be promoted to any class, for example String or Integer, and the classes it could be promoted to need not be in a supertype-subtype relationship. Therefore, having a value of type Bottom would allow contradicting type derivations to be made.
So if there is no value of type Bottom, what good is it? The same question came to my mind when I first encountered the Unit type: If there’s only one value, what good does returning it do? It doesn’t give me any useful information, because the answer is always the same. Actually, returning unit does convey information, even though the value is always the same: Returning unit tells the caller that the subcomputation is done. It doesn’t say anything what was done in that subcomputation, but whatever it was, it terminated. And giving something the return type Unit means that it will terminate. This sets the stage for Bottom: The return type Bottom means that a subcomputation will not terminate.
So, in short, there are no values of type Bottom because having those values would lead to contradictions. Returning Bottom conveys the idea that the subcomputation will not terminate, and that’s the difference to Unit: Returning Unit doesn’t yield any useful information beyond the fact that the subcomputation terminated.
Thinking about this made me realize that I claim that the empty record of invariants is a Bottom type. This is not true, of course, since the empty record is an actual value, and Bottom doesn’t have any values. What is true, though, is that the empty record is the bottom-most value that exists in my system. That’s close, but not exactly the same, so I’ll have to correct it in my thesis. I still have to think about whether the same applies to an invariant that is impossible to fulfill: The record describing it is an actual value, so can it be a Top type? I don’t think so, because there can definitely be more than one record of invariants that are impossible to fulfill.
The other issue that Justin brought up was schedule generation: He stated that not all permutations of synchronization points correspond to a valid schedule. I remember that I realized this over two years ago already, and that I brought it up in a discussion with Corky. I suggested that we use Lamport clocks, because that’s what the earliest relevant paper that I could find did. At that time, Corky convinced me that we can find a simpler data structure that still works: We just need a series of thread IDs to replay the schedule we have chosen.
I also remember being asked a question in the same direction by John Mellor-Crummey at a poster presentation. I embarrassed myself by not being able to answer the question; I could only say that I had thought about it. That was true, but I had forgotten my answer to it.
Corky is absolutely right that a series of thread IDs is sufficient to select a particular schedule; however, this approach only shifts the work from the replay algorithm to the schedule generation algorithm. There still is no free lunch. I agree with Corky, though, that reducing the work in the scheduler while increasing the work in the schedule generator is a good idea: Schedule generation can happen offline, and as long as the code does not change, the generated schedules remain valid. The scheduler, though, will have to do its work every time the code is run, so any work that can be removed from it saves computation cycles.
If we are to use the simpler data structure, we have to make sure that we only generate valid schedules, schedules that could actually occur “in the wild”. The only thing that can happen due to nondeterministic scheduling is that a different thread than usual is executed at a certain point. This means that, while the thread that is executing may change, the order of synchronization points within a thread have to remain the same. As a concrete example, consider the try-acquired-released sequence of synchronization points that corresponds to a synchronized block: It just doesn’t make sense to move the acquired event before the try event, or the released event before the acquired event, and so on.
Justin and I also discussed how we can reduce the number of synchronization points by ignoring those that occur during the execution of a certain method. Most likely, if you exclude synchronization points in one method, you also want to exclude those that occur in methods called by the method. To determine the synchronization points that should be ignored, we need to find the first fixpoint for the set described below:
- If the synchronization point to be excluded belongs to a structure of several of synchronization points, like the try-acquired-released sequence of a synchronized block, then the other synchronization points in that structure have to be excluded as well.
- If a synchronization point happens in the same thread as the synchronization points to be removed and occurs after the first synchronization point in that thread’s schedule and before the last synchronization point of that thread’s schedule, then this synchronization point has to be excluded as well.
Since the first rule may add synchronization points that happen earlier or later in the same thread, applying the first rule may make it necessary to exclude additional synchronization points, as per these two rules. The set of synchronization points is the set that does not add new members to the set, i.e. the first fixpoint.
I know I had already thought about this, perhaps not as concretely, but realizing this as quickly as Justin did is simply remarkable.
Another interesting thing began to emerge today in a discussion with Corky: In some cases, it may make sense to allow a stronger invariant, and a subtyping warning should not be emitted. It all depends on the static type that is used. If the program works abstractly with a supertype, then additional invariants added in a subtype should generate a warning to tell the programmer he is no longer maintaining substitutability. However, if the program actually works with the concrete type, then the program is probably aware of the stricter invariant because the object never gets treaded abstractly, and substitutability can be discarded. I’ll still have to look at that and work out examples, but right now it seems like this makes sense and is actually possible to implement, although it will make the instrumentation global, as now different call sites may have to be treated differently, depending on the concrete type. I also have to decide whether I am going to implement this now for my Master’s thesis or whether I am just going to discuss it. Right now, I definitely prefer the latter.
I also heard today that one of my committee members will be out of town at the end of June again, so I still don’t know if I’ll actually be able to defend in June. I still have to finish my slides anyway, though, and I feel like I can defend my thesis any day, so I don’t think this is a huge problem. I may have to defend earlier than I’d really want or later than I had planned, but it will happen.
Time to go to bed. Tomorrow, I’ll have to play around with a few examples.
PS: I think I’m now finally using the network-attached storage that I bought about a month ago the way I intended. Up until yesterday, I just never had the time or nerves to change my backup scripts.
