A few days back, Byron Cook, from Microsoft Cambridge came to give a guest lecture in the Formal Methods course. The guy, if you could call him that, talked about SLAM which Microsoft is now using internally for proving correctness of device drivers.
Amongst other things, he showed how, by using their software, the developers of Parallel Port device driver found two invocations of an IO completion API in a particular scenario. He said that a lot of Program Managers within Microsoft have started showing interest in Mathematical Logic and Formal Methods after Bill Gates personally congratulated the team. ;)
Other than increasing my interest further with Formal Methods, he talked about his former company, Prover Technology, which means that people are now building commercial products out of Formal Methods.
The lecture was quite complex keeping in view that we have just started studying this field of computer science. And this is one of the most complex fields within computer science; perhaps, as complex as Analysis of Algorithms. What I have learned uptil now starts from Propositional Logic and ends at First Order Logic. The lectures in this course will also cover Dynamic Logic but I still feel that we know nothing.
I have finally made up my mind to do thesis in formal methods and I have a few more months to start that. Fortunately or unfortunately, the Disrtributed Computing Research Group within Chalmers is not so active.
Saturday, February 26, 2005
Wednesday, February 23, 2005
Levels of Awareness
One of the most difficult concepts to explain in introductory science is the concept of life. What's the difference between living and non living things? Most of us have no answer except some heuristics that make us decide if something has life or not. And the line really blurs when we start discussing viruses! They are somewhere between living and non livings. Isn't it strange that we don't know what life is?
Don't expect that I'll give you an answer in this post! I am just giving you another perspective which is sometimes neglected. Do animals have "more life" than plants? Do plants have "more life" than the minerals they consume?
I expect that you'll agree that animals have stronger form of life than plants and we have an even stronger form of life as compared to other animals. And in my opinion plants have stronger form of life than minerals (I somehow believe that there is life in everything...it's just the strength of the form which is so weak that we don't consider anything else as living being, though I don't have any strong argument in favor of this claim).
Talking of the fellow human beings, aren't some of us more lively than others? So, what we might consider as "form of life" is actually degree of awareness - of yourself and your environment, though it's extremely difficult to say where exactly I start from and where I finish but let's postpone that discussion for some other time. I'll like to give some examples regarding degrees of awareness.
Suppose a child is asleep and sees a dream in which he looses his favorite toy. Then he wakes up and becomes worried; and when somebody asks him the reason, he tells about his dream. There is no doubt that everyone will try to explain him that it was just a dream - in other words, a difference between the reality and dream world.
Consider another child who is playing his favorite fighting game on his computer, in which he looses and starts crying. His elders will surely try to sooth him by explaining that it's just a game. However, if an elder behaves the same way while playing a game (he might be a real addict of gaming), you will be surprised, because you expect a different level of "awareness" from him. Suppose, he is not able to separate his identity from the game character that just died; won't life be quite difficult for him?
Now consider yourself and this real world of yours. What if someone comes to you and tells that you have bound yourself too strongly with your identity in this temporary world (compare with the gaming example in the last para)? Perhaps, it would be too difficult to understand mainly because the effort to make you aware of your real existence is from within this temporary world (as opposed to the gaming example).
Have you ever seen a dream in which somebody has told you that it's just a dream? I have! And not just once, it has become quite frequent. When this happens, it has some indication with it that convinces me that it really is just a dream - usually an unexplainable phenomenon such as the hands of a clock moving in the opposite to usual direction, etc.
[to be continued...will write after learning more about life...]
Don't expect that I'll give you an answer in this post! I am just giving you another perspective which is sometimes neglected. Do animals have "more life" than plants? Do plants have "more life" than the minerals they consume?
I expect that you'll agree that animals have stronger form of life than plants and we have an even stronger form of life as compared to other animals. And in my opinion plants have stronger form of life than minerals (I somehow believe that there is life in everything...it's just the strength of the form which is so weak that we don't consider anything else as living being, though I don't have any strong argument in favor of this claim).
Talking of the fellow human beings, aren't some of us more lively than others? So, what we might consider as "form of life" is actually degree of awareness - of yourself and your environment, though it's extremely difficult to say where exactly I start from and where I finish but let's postpone that discussion for some other time. I'll like to give some examples regarding degrees of awareness.
Suppose a child is asleep and sees a dream in which he looses his favorite toy. Then he wakes up and becomes worried; and when somebody asks him the reason, he tells about his dream. There is no doubt that everyone will try to explain him that it was just a dream - in other words, a difference between the reality and dream world.
Consider another child who is playing his favorite fighting game on his computer, in which he looses and starts crying. His elders will surely try to sooth him by explaining that it's just a game. However, if an elder behaves the same way while playing a game (he might be a real addict of gaming), you will be surprised, because you expect a different level of "awareness" from him. Suppose, he is not able to separate his identity from the game character that just died; won't life be quite difficult for him?
Now consider yourself and this real world of yours. What if someone comes to you and tells that you have bound yourself too strongly with your identity in this temporary world (compare with the gaming example in the last para)? Perhaps, it would be too difficult to understand mainly because the effort to make you aware of your real existence is from within this temporary world (as opposed to the gaming example).
Have you ever seen a dream in which somebody has told you that it's just a dream? I have! And not just once, it has become quite frequent. When this happens, it has some indication with it that convinces me that it really is just a dream - usually an unexplainable phenomenon such as the hands of a clock moving in the opposite to usual direction, etc.
[to be continued...will write after learning more about life...]
Sunday, February 20, 2005
Karbala
At the expense of redundnacy, I say that the amount of information obtained from an event is directly propotional to its rarity. And Karbala is an event which is the rarest of its kind in the history of mankind. Despite the fact that the exact details have reached us, most of the people just have a very vague idea of Karbala.
Quoting from one website:
Each and every detail associated with this happening is enlightening. Consider, for example, what made the "Muslims" fight against the grandson of the Holy Prophet (sal'Allaho alayhe wa'alayhi wasallam)? This happened in less than 50 years after Prophet's (PBUH) death!
Why Husain bin Ali (AS) took only 70 people with him when he was leaving Madina? While Husain (AS) refused many people who wanted to go with him, he wrote letters to some others to accompany him! The list of such people includes Habib bin Mazahir, a childhood friend of Husain (AS), who was more than 70 years old then.
Each and every act and saying in this few days period seems to be planned as if to teach us something. Consider Hur, the leader of a small section of the evil forces, who changed sides just a night before and joined Husain's (AS) camp. He knew fully that the stage had been set and the next day every man on Husain's (AS) side would be martyred. Hur would not have changed sides if Husain (AS) had not asked the evil forces to delay the fight for a night.
The companions were handpicked. A night before Ashura, Imam Husain (AS) said, "Tomorrow whoever is here will die so I let you go away from here; save yourself; I permit you to leave this place." When nobody left, he ordered the light to be put off so that nobody was ashamed of leaving in front of others. But in reply all of them said, "If we are to die seventy times and our bodies are burnt even then we will not leave you."
No saint or Prophet had such companions! And perhaps the night of Ashura was the strangest in human history, when the companions and Husain (AS) spent the whole night offering prayers to Allah. Not a single drop of water had passed through the throats for the past 3 days; the happenings of the coming day were known to all; yet, they showed so much calmness! so much generosity! Perhaps, this would have been a night when angels would have desired to be such humans.
I dare to say that if you don't know Karbala, you know nothing about life. You are asleep and need to wake up.
بیاں سر شھادت کی اگر تفسیر ھو جاۓ
مسلمانوں کا کعبہ روضہُ شبیر ھو جاۓ
(علامہ اقبال)۔
Quoting from one website:
Ashura is the story of loyalty, bravery, piety, magnanimity and self-sacrifice. It is the eternal saga of persons who created epics to safeguard humanitarian principles so that the coming generations can live in dignity with heads held high in defense of truth. On this day, the Prophet’s grandson courted martyrdom in order to inspire mankind in the fight against injustice and exploitation. In the words of American historian Washington Irving the spirit shown by Imam Hussein (AS) remains immortal since he presented the lasting example of heroic bravery.
Each and every detail associated with this happening is enlightening. Consider, for example, what made the "Muslims" fight against the grandson of the Holy Prophet (sal'Allaho alayhe wa'alayhi wasallam)? This happened in less than 50 years after Prophet's (PBUH) death!
Why Husain bin Ali (AS) took only 70 people with him when he was leaving Madina? While Husain (AS) refused many people who wanted to go with him, he wrote letters to some others to accompany him! The list of such people includes Habib bin Mazahir, a childhood friend of Husain (AS), who was more than 70 years old then.
Each and every act and saying in this few days period seems to be planned as if to teach us something. Consider Hur, the leader of a small section of the evil forces, who changed sides just a night before and joined Husain's (AS) camp. He knew fully that the stage had been set and the next day every man on Husain's (AS) side would be martyred. Hur would not have changed sides if Husain (AS) had not asked the evil forces to delay the fight for a night.
The companions were handpicked. A night before Ashura, Imam Husain (AS) said, "Tomorrow whoever is here will die so I let you go away from here; save yourself; I permit you to leave this place." When nobody left, he ordered the light to be put off so that nobody was ashamed of leaving in front of others. But in reply all of them said, "If we are to die seventy times and our bodies are burnt even then we will not leave you."
No saint or Prophet had such companions! And perhaps the night of Ashura was the strangest in human history, when the companions and Husain (AS) spent the whole night offering prayers to Allah. Not a single drop of water had passed through the throats for the past 3 days; the happenings of the coming day were known to all; yet, they showed so much calmness! so much generosity! Perhaps, this would have been a night when angels would have desired to be such humans.
I dare to say that if you don't know Karbala, you know nothing about life. You are asleep and need to wake up.
بیاں سر شھادت کی اگر تفسیر ھو جاۓ
مسلمانوں کا کعبہ روضہُ شبیر ھو جاۓ
(علامہ اقبال)۔
Sunday, February 13, 2005
Tuesday, February 08, 2005
Minesweeper is NP-Complete
Surprising but it's true that Minesweeper is NP Complete. If you remember the definitions from your Algorithms/ Complexity Theory course, to prove that a problem X is NP-Complete you need to reduce a well-known NP-Complete problem (usually satisfiability problem) to X in polynomial time. Solving any NP-Complete problem in polynomial time means that all Non Polynomial time problems would be solved.
And if you can't recall what NP was, let me remind you that problems which require exhaustive analysis of all possibilities to find the best solution are Non Polynomial time. And if you are as dumb as me you will need an example to understand this: Suppose you want to check if a string A is a substring of B and assume that the only possible method is to generate all possible substrings of B and match A against each one of them, then string matching would have been an NP problem.
Some Sokoban addicts seem to be interested in proving that their game is even more complex.
With this comes the "Is P=NP?" question. It's one of the Millennium Questions; there is $1 million award for the person who answers it with mathematical precision.
To this day, I fail to comprehend the difference between NP Complete and NP Hard. Also, some problems are said to be NP Complete in the strong sense. Can any enlightened reader shed some light?
Today, we have CHARM day at Chalmers. The industry comes to interact with the students. After many days of inactivity, once again, I am starting exercise and better time management from today.
And if you can't recall what NP was, let me remind you that problems which require exhaustive analysis of all possibilities to find the best solution are Non Polynomial time. And if you are as dumb as me you will need an example to understand this: Suppose you want to check if a string A is a substring of B and assume that the only possible method is to generate all possible substrings of B and match A against each one of them, then string matching would have been an NP problem.
Some Sokoban addicts seem to be interested in proving that their game is even more complex.
With this comes the "Is P=NP?" question. It's one of the Millennium Questions; there is $1 million award for the person who answers it with mathematical precision.
To this day, I fail to comprehend the difference between NP Complete and NP Hard. Also, some problems are said to be NP Complete in the strong sense. Can any enlightened reader shed some light?
Today, we have CHARM day at Chalmers. The industry comes to interact with the students. After many days of inactivity, once again, I am starting exercise and better time management from today.
Saturday, February 05, 2005
Adlerbertska Scholarship
The education system in Sweden is strikingly different from the US (and thus from Pakistan as well). Though they may start charging tuition fee in the next few years, at present they don't - not even from International Students. This has very far reaching affects. Not only that we don't pay the university, we enjoy the same facilities as the local students and each term the university arranges some outdoor activity for the International Students, again free of cost. We have been to Universeum and Gothenburg Opera in the last two terms.
Such an attitude has deep roots in Europe - the culture is of caring and sharing. Perhaps, that's why Europe has most contributors to the Open Source work, around the world. Though there are people who would like these countries to be like the US, apparently such people are very few in number.
In Gothenburg, there used to live a man called Axel Adler (1878-1966). He started working at the age of 7 and later joined the family business of dairy products. He became the company director at the age of 24. After mid-life career, he started studying again; got married; lived in Gothenburg; rejoined family business; restarted studies and finally had a vision for Gothenburg: "a living university town where young people would have access to a rich centre of knowledge and cultural activity." If you visit this small city you will agree that his dream has materialized. Back in his days, he opened a local library in his home and held seminars in many subjects. His farm-house became a centre of new ideas that drew lecturers from the whole of northern Europe.
He established several foundations and to this date, every year one of his foundations gives approximately SEK 4000 to every foreign student who comes to study in Gothenburg. This might seem like a small amount (about Rs. 30K) but consider giving it every year to about 900 students, without any kind of discrimination, just for coming to Gothenburg for their studies!
Such an attitude has deep roots in Europe - the culture is of caring and sharing. Perhaps, that's why Europe has most contributors to the Open Source work, around the world. Though there are people who would like these countries to be like the US, apparently such people are very few in number.
In Gothenburg, there used to live a man called Axel Adler (1878-1966). He started working at the age of 7 and later joined the family business of dairy products. He became the company director at the age of 24. After mid-life career, he started studying again; got married; lived in Gothenburg; rejoined family business; restarted studies and finally had a vision for Gothenburg: "a living university town where young people would have access to a rich centre of knowledge and cultural activity." If you visit this small city you will agree that his dream has materialized. Back in his days, he opened a local library in his home and held seminars in many subjects. His farm-house became a centre of new ideas that drew lecturers from the whole of northern Europe.
He established several foundations and to this date, every year one of his foundations gives approximately SEK 4000 to every foreign student who comes to study in Gothenburg. This might seem like a small amount (about Rs. 30K) but consider giving it every year to about 900 students, without any kind of discrimination, just for coming to Gothenburg for their studies!
Thursday, February 03, 2005
Assignments: Concurrent Programming and Formal Methods
One of the most famous assignments in DCS program at Chalmers is Train Control in the Concurrent Programming course. Apparently, it's a very good way of learning about critical sections and locking. It can also be extended to classical problems such as readers and writers by drawing the tracks in a different way. But the problem with the assignment is that when you apply brakes, the trains don't stop immediately. They slow down gradually and the time they take to come to a halt depends on their speed. Having the goal to run the trains at the maximum possible speed while managing to brake right before entering the critical section makes the assignment hard and, for me, very boring. It took me one day and one whole night at the university to complete it.
Another assignment that took most of the time last week was to simulate an elevator. We had to write it in Lustre. Chalmers has one of the finest teams in the world when it comes to formal methods for software. One of the Associate Professors, Koen Claessen, has hacked Luke that we use instead of the compiler from the authors of Lustre. Luke generates an HTML page from a Lustre file with all propositional logic embedded into it. It's very interesting. Another tool, KeY, also developed at the university, is used for complex automated verification of software properties.
If life and time permits, I intend to introduce some of these courses when I go back to Pakistan.
Another assignment that took most of the time last week was to simulate an elevator. We had to write it in Lustre. Chalmers has one of the finest teams in the world when it comes to formal methods for software. One of the Associate Professors, Koen Claessen, has hacked Luke that we use instead of the compiler from the authors of Lustre. Luke generates an HTML page from a Lustre file with all propositional logic embedded into it. It's very interesting. Another tool, KeY, also developed at the university, is used for complex automated verification of software properties.
If life and time permits, I intend to introduce some of these courses when I go back to Pakistan.
Subscribe to:
Posts (Atom)
Posts
