It has been a while, but now I have green tomatoes:

Amazing.

External Content not shown. Further Information. Tröööt! There is a new protocol joining the small group of network protocols which I like. The Network Block Device protocol. It seems like it is exactly as complicated as it needs to be. It just has a major disadvantage: It is not well documented. Surprisingly, the German Wikipedia has a quite nice article about NBD, and this article is not that bad! It even has a protocol documentation - as one wishes when consulting an encyclopedia. (So it will probably be deleted soon.)

Actually, I had a closer look at NBD while I was actually looking for something else, but the implementation of an NBD server took some time. I wanted to create an NBD server which allocates a specified amount of memory and populates it as block device - just as a proof of concept telling me that I have "understood" the protocol and that I am able to implement it.

I began with C and finally succeeded, after finding out that every adress has to be sent in network byte order, and finding some useful header files like <linux/nbd.h>. Still, my C implementation has some bug, and as I did not have any special aim, I re-implemented everything in Common Lisp. The code can be found at GitHub (exercise: find out where its name comes from).

Its only dependency so far is usocket, and as I did not yet create an asd file it has to be loaded manually, which I do via Quicklisp.

CL-USER> (ql:quickload "usocket")

Then I load my file and start a server with a 10 megabyte block device.

CL-USER> (load #P"~/projects/7-chloro-4-nitrobenzofurazan/nbdserver.lisp")
CL-USER> (defvar *pool* (run-rampool 13337 (* 10 1024 1024)))

This will block until an nbd client connected and returned again. So let us connect via the linux nbd client. We create an ext2 filesystem and then mount it and create a file GANS with the content NILPFERD in the shell

# nbd-client localhost 13337 /dev/nbd0
Negotiation: ..size = 10240KB
bs=1024, sz=10240
# mkfs.ext2 /dev/nbd0
[...]
# mount /dev/nbd0 /mnt
# echo "NILPFERD" > /mnt/GANS
# sync
# cat /mnt/GANS
NILPFERD

Then we unmount it again and detatch the device.

# umount /mnt
# nbd-client -d /dev/nbd0
Disconnecting: que, disconnect, sock, done

Now, the REPL is free again, and *pool* contains the data. We have just created an ext2 filesystem on a lisp vector. Now we should find the word "NILPFERD" in *pool*, and indeed

CL-USER> (search (map 'list #'char-code "NILPFERD") *pool*)
2098176

Now let us see what happens if we replace this string (as this returns the whole *pool*, we set *print-length* first):

CL-USER> (setf *print-length* 10)
10
CL-USER> (replace *pool* (map 'list #'char-code "nilpferd") :start1 2098176)
#(0 0 0 0 0 0 0 0 0 0 ...)

Now, let us re-run the nbd-server with the modified *pool*

CL-USER> (run-rampool 13337 (* 10 1024 1024) *pool*)

And attatch and mount it again

# nbd-client localhost 13337 /dev/nbd0
Negotiation: ..size = 10240KB
bs=1024, sz=10240
# mount /dev/nbd0 /mnt

Now, about the file:

# cat /mnt/GANS
nilpferd

Yep, it is indeed lowercase now. Which is ... nice ... somehow. Though useless, of course.

Besides that, I found an implementation of a server in python, though I have not tested it. Same for this Java implementation.

Unfortunately, there seems to be a lack of clients. A port to some other Unices and Windows would be nice. Especially, looking at these implementations of block device drivers, there should be people who can easily implement an NBD Client for Windows.

As the German Wikipedia keeps getting destroyed by arrogant pimple faced pubescent high schoolers, unlike the English Wikipedia, there is no article about the Glivenko Theorem in the German Wikipedia anymore. As far as I remember, there has been one in the past. Currently, this article in the English Wikipedia is suggested to be merged with the article about the Gödel Gentzen Negative Translation, which sounds reasonable, as it is a generalization - but it also does not have an article in the German Wikipedia anymore.

The German Wikipedia does not have any form of the quality it used to have. There is no "freedom" anymore: The last time I edited something, it took weeks (!) for the article's usurper to confirm my changes. I do not see the "freedom" it proclaims anymore.

Besides general boredness, I take that as an occasion to blog about the Glivenko Theorem. Especially, I want to try out how good (or bad) I can get MathJax to produce proof trees. Apparently, it does not look so bad, but there is no real possibility to create horizontallines, stuff like \cline does not work in MathJax. If someone has suggestions on how to make them look better, please let me know. I am using my own pre-generated HTML tables currently, which look good, but I would prefer a solution that is more integrated into MathJax.

Especially, this post's primary purpose is to be informative for people who were not concerned with logic so far. Every mathematician should already know everything stated here.

The Glivenko Theorem sais that in propositional logic, if P→Q is provable classically, then ¬¬P→¬¬Q is provable intuitionistically.

There are several ways to prove this. But let us first look at what that means.

In the end, a sufficiently simple calculus for this is the Hilbert Calculus, which only implements Modus Ponens, that is, has only one rule: From A and A→B we may derive B. Additionally, if we have a proof of B from A, we may derive A→B and strike A from the list of axioms.


We get intuitionistic propositional logic by the axiom schemes (→ is right-associative and binds less strict than ∨ and ∧)


Furthermore, we introduce a special propositional symbol ⊥, the falsum, and add the axiom of ex falso quodlibet


which means that from a wrong proposition we may derive everything.

For classical logic, we define ¬A:=A→⊥, "not A". Then to get classical logic, we add the axiom scheme of duplex negatio affirmat

which becomes


in the above notation.

To prove the Glivenko Theorem, we show that every rule and axiom for classical logic is derivable in double-negated form in intuitionistic logic. Therefore, the first thing we shall prove is that from ¬¬(A→B) and ¬¬A we may derive ¬¬B, corresponding to the modus ponens. In words, the proof goes:
Assuming A→B and ¬B, we know that ¬A must also hold, which contradicts ¬¬A. Therefore we know that one of our assumptions is wrong. Assuming ¬(A→B), we get a contradiction with ¬¬(A→B). Therefore, the assumption ¬B must be wrong, therefore ¬¬B.

Formally, it goes:
Furthermore, we need to show that if ¬¬B can be implied by ¬¬A, also ¬¬(A→B) holds. So let us assume that ¬¬B follows from ¬¬A, but ¬(A→B). Assuming ¬A holds, using ex falso quodlibet ⊥→B gives us A→B which contradicts ¬(A→B). So ¬¬A which implies - by assumption - ¬¬B. Now, assuming B, we can follow A→B, which also contradicts ¬(A→B), so ¬B. But ¬¬B and ¬B contradict each other. So ¬¬(A→B). I admit, this proof is somewhat hard to understand. Here is the formal tree:


Notice that from B we followed A→B. This is correct according to the above definitions, but maybe not clear immediately.

An easier proof can be given for A→¬¬A, which we need to be able to convert all of our additional axioms for the junctors.

Finally, we need ¬¬(¬¬A→A) to be derivable, and by the above proof, it is sufficient to prove ¬¬¬¬A→¬¬A, because that is ¬¬(¬¬A)→¬¬(A) and therefore implies ¬¬((¬¬A)→(A)). It can be derived by:


We have proved the Glivenko Theorem. W00t.

The feel when diving into a virtual world. For a healthy person it can be relaxing, for a disabled person, I guess it can be a form of escape from his body.

Unfortunately, while those who would be able to go outside are given several kinds of gadgets, those who cannot appear to be widely forgotten by the game industry.

How refreshing to read that there is some person who cares. Of course, this is not the first time I hear of disabled gamers but this time in a completely different manner.

One may ask whether quadriplegic people do not have more important problems - at least this is a question I expect from the ordinary™ person. Actually, most people have more important problems than gaming, regardless of whether they are disabled or not. But thinking about it, I actually do not know anything I could do without moving. I do not like to walk, I do not like to get up, but I am aware and thankful that I can. Without this ability, what can you do all the day? You cannot eat without help, you cannot even read a book yourself, without some gadget that helps you. Playing a video game, getting a bit of the feeling of being able to move, I am pretty sure that this can make a disabled person less depressed. And there are games that can be played together. In the virtual world, they are not disabled anymore.

Above that, let us not forget that these controls, and the expierience with it, might soon or later help developing better gadgets for real life for those people.

Today was the first time that I ran into an unexpected race condition. With a bash script for a self made automounter. The automounter is invoked by udev. I did not expect udev to run the same script twice parallely, and so, an error occured.

The theoretical solution is simple, use locking. But in fact, I never have seen bash scripts doing something beyond

[ -e my_lock_file ] || touch my_lock_file && ...

to create locks, and this is dangerous, because between testing and touching a logfile, there might be the time for another test - the locking is not atomic.

I would have been surprised if this problem did not have a solution, and in fact, it does:

lockfile-create /tmp/my.lock
...
lockfile-remove /tmp/my.lock

Nice. Especially, it allows simple experiments with lockfiles through remote file systems.

In my school, there were a lot of projects trying to tell pupils how to do successful learning. Some of them were useful in special settings, but most of them were just ignored by most students, like me.

One example is the record card based learning of vocabulary. I always hated learning vocabulary, because it is just plain memorizing, there is no understanding behind it. Additionally having to maintain a bunch of cards never really helped, actually, I found it even more annoying to learn them. At that time however, computer aided vocabulary trainers were not yet widespread, maybe a record card based learning strategy is more helpful with a computer.

Even worse was everything regarding social sciences, history for example. I would have been glad if it just had been about learning dates and names. But additionally, it was about reading and "understanding" the stupid opinions of posers and explaining one's opinion (or at least the opinion the teacher wants you to have) to them.

While I never really had problems in science, I saw several people having problems because they simply did not find any way of seeing how science works. In everyday life, there is no need for proper definitions or fireproof reasoning as it is when doing science. You are rolling around opinions of yourself and others, but you have no need to prove them in an empirical or logical way, and learning to do this would probably be better than knowing the periodic table by heart.

So, well, I have done school, and I know others who have. I know people who were quite good, and I know people who were quite bad. I guess this gives me at least some eligibility to write a blog post about successful learning. However, I can only give suggestions, everybody must find his own way - probably the first thing to know: If you have found your own learning strategy, then keep it, even though others tell you it is bad.

The main lack regarding most recommended learning strategies I have seen is that they address exactly one thing very well. Namely the fact that if you practice things often enough, you will remember them. I cannot remember any learning strategy not being focused on efficient memorizing of matter. They give a way of learning certain kinds of matter fast. But they miss one crucial point: The personal interest.

No matter how hard I try, it is hard to learn something I do not really want to know. For some people, getting good grades is enough motivation to be willing to know matter. And in my expierience, the people with a better average grade were usually the people who did not really have any deeper interest in the actual matter but getting good grades. Just to make that clear, I am talking about the better people, not about the best people. And I am not talking about "nerdy" pupils who do not have any hobbies except learning for school, I am only talking about their interests regarding school matter.

So before you even try to make your learning more "effective", ask yourself whether you really want to be good at the certain subject. Ask yourself, why do you learn for that subject. It can be hard to be honest to oneself, so take your time thinking about it.

Maybe you have a deeper interest for the subject - which does not mean that every of your grades needs to be perfect. I had a deeper interest in Mathematics, still, my grades were not always perfect. School can also underchallenge you, and you should never forget that every school subject can be separated in a lot more subjects, and even if you like one subject in general, there may be parts of it that you do not like (like stochastics for me).

Still, if you have a deeper interest, then you should be able to learn it quickly, and therefore you should do so. And you should not stop at the level of current school matter: If school is too slow for you in a certain subject, try to get further information on it - books for the next class for example, or even university books, if you are good enough. Almost every subject has its own competitions on which pupils can take part. Even if you are not good enough to win a prize, participate, just to show other people that you are interested!

If a teacher notices that you become good at something, depending on how much of an asshole he is, he either will support you - then you should take this support and be thankful - or he will try to get you away from doing this - then you should ignore it. Do not try to discuss with teachers, you can only lose, and if you lose, you will probably lose more than just a discussion. Life is hard and cannot be lived without some kickbacks, and if you cannot manage to achieve all your goals, do not expect teachers to be able to console you. Some teachers may be able to, but some will also be glad about your failures, especially when they tried to keep you away from something before. Expect this. Teachers are just human, in the end. The older you get, the thinner becomes the facade of wisdom they want their pupils to see. And you are a factor that creates additional work. Keep that in mind.

Now, let us assume you have such a subject, then if you do not suck completely at everything else, you will probably not be the best of all pupils, but your grades will be sufficient for most things you want. There is no need to become good at everything.

In case you do not have any subject of interest, but you still do not feel successful enough, you should wonder why you go to school at all. Make up your mind about what you want to achieve. If it requires finishing the school you go to, then you should be able to find at least something interesting, because that usually means that school should teach at least some skill that is needed. If you do not think so, then you are probably missing something about your plans.

If you do not have any plans at all, then it is still better to finish school, to have a broader range of possibilities later. Then you will just have to learn to ignore your boredness while learning. This is probably the hardest part, because the usual learning strategies cannot handle this situation, they all assume that you actually want to learn the matter rather than being forced to.

They usually tell you not to have things that may distract you from learning. But presumably you are familiar with the situation that even though you try to keep away distracting things, you will find everything distracting if you do not really want to learn. The solution is simple: Have something that distracts you while learning. Do something else while looking at the matter. This is quite the opposite of what almost every learning strategy will tell you, and in fact, you will not even learn half as much as you could when just concentrating on the matter. So if you can manage to concentrate on it try to do it, but since concentrating on the matter is not always possible, having something distracting is basically the best possibility to find a balance between your boredness and your duty. Your grades will probably not be the best, but they should always be sufficient.

Trying to enforce your interest on a topic will fail, you can try to find something interesting in a topic, but if you cannot find anything of interest, you just have to accept that. Man can do what he wants but he cannot want what he wants, as Schopenhauer said.

And - even more important - never rely on teachers to make something more interesting to you. Probably there are some teachers who are able to achieve this. But mostly, either the teacher is pretentious and therefore not willing to give you instructions on why his or her subject is interesting, and therefore might hate you from the day you have asked, or he is not even interested himself. I coached pupils while I was still at school, and I have marked tests of teacher trainees at the university - I can say that at least in Germany, the latter case definitely occurs. Very often.

You may have noticed that I gave a quite bad image of teachers. Teachers are, as I said, humans. Teachers are the persons who give instructions to you - some of them enjoy their job, some of them hate their job. In any case, they are your instructors, not your friends.

You may like them on a personal level, as soon as you get old enough to have them let you know more about their personality. I have talked to teachers outside school, and some of them had quite interesting personalities. Of a few of them I even wondered how such a friendly person in real life can be such a dick during the lessons.

But that is how it is: They might be enjoyable in real life, but at school, which is clearly not real life, they are your instructors, not your friends. They have work to do, and you are part of the material they work with, and if you are difficult to handle, that is more work for them.

I hate firewalls, but I have no choice, with gigabytes of spam-traffic. By a mistake of mine, I probably locked out a lot of IP adresses that should not have been locked out. I am sorry for that.

If you notice that I locked somebody out, please let me know.

There is apparently no simple possibility to find out whether a given IP adress is blocked. So I cannot easily filter my logfiles. Above that, the default whois-answer gives an IP range, but iptables wants CIDR-notation.

I could not find any software calculating this (if somebody knows a good one, then please tell me). What I quickly wrote in a file range2cidr.c is:

#include <stdio.h>
#include <stdlib.h>
#include <unistd.h>
#include <string.h>
#include <stdint.h>
#include <netdb.h>
#include <math.h>

int main (int argc, char ** argv) {
  if (argc != 3) {
    printf("Usage: %s lowerbound upperbound\n", argv[0]);
    exit(EXIT_FAILURE);
  } else {
    uint32_t lowip, highip;
    struct hostent *host;
    host = gethostbyname(argv[1]);
    lowip =
      ((((uint8_t) host->h_addr[0]) % 256) << 24) +
      ((((uint8_t) host->h_addr[1]) % 256) << 16) +
      ((((uint8_t) host->h_addr[2]) % 256) << 8) +
      ((((uint8_t) host->h_addr[3]) % 256));

    host = gethostbyname(argv[2]);
    highip =
      ((((uint8_t) host->h_addr[0]) % 256) << 24) +
      ((((uint8_t) host->h_addr[1]) % 256) << 16) +
      ((((uint8_t) host->h_addr[2]) % 256) << 8) +
      ((((uint8_t) host->h_addr[3]) % 256));

    uint32_t msk = lowip ^ highip;

    int i=0;
    while (msk != 0) {
      msk /= 2;
      i++;
    }

    printf("%s/%d\n", argv[1], 32-i);
           
    exit(EXIT_SUCCESS);
 
  }}

You might wonder why I calculated the IPs so high-level. Well, I just did not want to care about the whole lowlevel-fuss and still have it portable - I mean, this code does not need to be fast, it just needs to be correct.

Anyway, there has got to be better software. Any suggestions?