Exactly. But the problems go beyond that. For instance, I gave a speech on the Pledge of Allegiance. Imagine if it were a paper. How am I supposed to write this? Say "The Pledge of Allegiance is a statement that the speaker promises allegiance both to the US flag and the US itself, states that the US is a single nation beneath a diety, and that it offers liberty and fairness to all"? Then what? "The original form of the pldege, passed in 1892, only had the speaker promising allegiance to the flag and to the US, a single nation that offers liberty and fairness to all."?
I'm going to go out on a limb and say that I don't think you can write a decent paper without quoting. There are occasional exceptions; research papers (as in the "getting published in a journal/conference" sense of "research") often don't have quotes, though often have a lot of self semi-plagiarism.
If that's the case, then why don't they use a BSD-like license? Because that's all they will have if copyrights are eliminated -- anyone can take FSF code, modify it, and lock away their modifications.
In such a world, the "locking away" would be through technical, not legal, means. If someone did that, you could still reverse engineer their software, distribute their software, etc., but this wouldn't be possible today with the BSD license.
The GPL does depend on copyright, but they are using it as a means to an end in some sense. They would rather have software copyrights abolished entirely than keep the GPL around.
So saying that the FSF has an "open and virulent bias against copyrights" clearly demonstrates either a lack of research, a lack of understanding, or a lack of honesty on the part of the RIAA's lawyers.
I'd say your comment illustrates one of those things on your part; the RIAA's description in that part is actually pretty accurate.
Burn fuel != burn as much fuel. They should be able to be made more efficient than probably anything else out there on a per-person, per-mile basis. I don't know how they stack up now though, but I would bet they're better than driving.
This causes very, very frequent delays for passengers. Enough so that many won't take the train.
It's basically stopped me.
My last Amtrak experience was a big pain. I was going from Chicago -> Pittsburgh, then catching another train from Pittsburgh. There was a freight derailment east of Chicago that basically shut down Amtrak traffic entirely, so Amtrak had to put together busing for us around the derailment. So we bussed from Chicago to Toledo, then got onto the train. At that point, if we had made it to Pittsburgh in the amount of time it was supposed to take, I *might* have been able to make the connection. We would have been coming in around 1 1/2 hours after the connection was supposed to leave, and on an earlier train ride a guy said he had ridden the train a lot, and had often seen Amtrak delay that train by an hour or two so people would make their connections. For about half of the Toledo->Pittsburgh distance, it actually looked like we'd make it... but then we sat outside of Cincinatti, not moving for over an hour. I strongly suspect that it was freights that were delaying us. By the time we got moving, there was basically no hope, and of course the train had left by the time we arrived. So basically, even though it was the fault of the freights that we were put in that situation in the first place, they still cost me a missed connection. (At that point, rather than bus for a couple more hours I just had them refund that part of my ticket, which they did no questions asked.)
I was actually moderately impressed with the way Amtrak handled what they were given; with a couple somewhat minor exceptions, there were actually mostly on the ball. (We got out of Chicago an hour late. The main problem there was that while we were actually mostly on the buses at the scheduled departure time, we then sat around for an hour waiting for some paperwork stuff apparently. Did that cost me the connection too? Very possibly.) Certainly miles better than most US airlines would have been. ("Not our fault; you're on your own until our next flight tomorrow.")
(You did forget the other main legitimate complaint -- it's slow. It's often as fast or faster to drive. When I went home by train, because of the way things work out it was about 24 hours to go by combination bus/train; driving would have been ~12 hours.)
For those of you, like me, that read TFA and the article linked from TFA and still don't know what Phorm is other than it's something that some UK ISPs are implementing and there appear to be privacy concerns, Wikipedia.
In short, it's system for doing targeted advertising by deep-packet inspection.
RAID isn't replication, and it isn't backups. SCSI is just an interface for talking to disks. You really need something at a higher level to be able to get true replication. Backups can be it, but you need to be sure that you get a consistent image of the DB. If you just naively copy bytes, it's very easy to not get this. If you just naively lock the file while you back up, you kill Exchange. Doing something that isn't one of those things either needs COW support from the OS or it needs cooperation from the actual application (Exchange).
Just to counter the other reply, I would say that I, all of my friends, and most of the people who I've heard opinions of second-hand have said it's just a great game. Personally, I felt largely the same sort of "wow, this is really cool" feeling I got when playing Portal. (Not quite the same because I didn't get the same sense of "this would be really cool to do in real life" or anything like that, just from a gameplay sense.)
(And the soundtrack is not an integral part of the game from a gameplay sense, but it is great from a ambiance sense, and the way it works into the time mechanic is just really well done.)
How tied to Java is Android development? Is that the only option, or could I write in some other language if I wanted? (I don't care about C; I'm more interested in something like Python, Lisp/Scheme, and O'Caml.)
So, groundbreaking in some minor ways, but really just a continuing in the same efforts at formal proofs which have been going on for thirty or forty years now.
All research continues something that came before. "If I have seen further than others, it is because I have stood on the shoulders of giants" and all that. If you want to argue about the meaning of groundbreaking, whatever, but it's as groundbreaking as anything in software formal methods in the last couple decades.
Perhaps they are groundbreaking in that they can be applied to MSWindows 7, whereas the previous methods were more taylored to previous MS OSses (or to other OSses).
The methods they describe aren't tailored to ANY MS OS, though the implementation is. SLAM was groundbreaking because there wasn't anything that did anything even somewhat close to what it did, for any system ever.
I don't really have time to address the rest of your post now; it's late. I may get back to it tomorrow.
Maybe these tools will help generate "correct" code for some definition of correctness. But have these guys defended their choice of definition of "correctness"?
A little bit. There are two bits of how they would need to justify it: is it guaranteed to make sense, and how complete/useful it is.
The first bit is easy: the sorts of things they check for are the sorts of things that cause program or system crashes, or other clear failures. A null pointer dereference is almost always an error. Trying to lock an already-locked mutex is always an error if it's not designed to allow that. In a device driver, making a potentially-blocking function call while interrupts are disabled is always an error. (This is true on both Linux and Windows.)
The second bit, showing that proving a program is free of these errors is useful, is a little harder, because there's no program- or driver-specific behavior they can check. They can't figure out that, for instance, a program would produce incorrect output. If a calculator says that 1+1 is 3, SLAM wouldn't be able to tell you that is wrong. This problem is mitigated somewhat by the fact that SLAM takes as input a specification of the property that you want to prove, so if you DO have an application-specific check you want to make, there's a chance you could express it as something SLAM could check. No guarantee however.
At the same time, how many people around/. do you see complaining about Windows blue screens? Even now that they are relatively rare (I haven't seen one in ages despite running Windows on two computers I use regularly), crashes still spur complaints. So I would argue that yes, the definition of "correctness" they use IS useful in its own right.
And I wouldn't be alone; this is basically the current state of program analysis. Proving that a program actually does what it is supposed to is generally seen as out of reach, at least for now. (I would argue that it will be in the future too. For most programs, specifying what it means for a program to actually do what it is supposed to would require a specification on the same complexity order as the code itself. What's a formula that describes what Word is supposed to do? Or Emacs? Or Firefox?) There are tons and tons of papers out there that use some measure of correctness comparable to what the SLAM project used. One example that comes to mind is some stuff on concolic execution that came out of Lucent Labs and UIUC (Dart and the followup work Cute) that uses a definition of correct that includes things like null-pointer dereferences, divisions by zero, or the program reaching an assert statement. Again, there's no application-specific behavior that it knows about (unless you encode it in the program itself in an assert; presumably SLAM could pick this up too). But there are many other examples.
Is the application field a niche field, or will it help with OSses and general end-user applications?
How much it will help is still up in the air. Right now all of the verification methods out there are limited to very small programs. (This is the primary reason that the SLAM project targeted device drivers -- they tend to be very small.) So you won't be able to verify the whole OS any time soon, and you won't be able to verify anything but the smallest utilities.
But today's techniques actually DO work on device drivers. SLAM has been packaged up with the Driver Development Kit starting a bit over 2 years ago, and IIRC MS has added it to the WHQL driver certification process. I have no idea how much it actually helps in practice though. (It certainly has the potential to; most of Windows crashes are caused by third-party drivers.)
(There are other program analysis techniques that DO scale to large (millions of lines) programs. However, they are neither sound nor complete, so they aren't guaranteed to catch every bug and can also return l
A fair amount of ground-breaking research. The SLAM project and followup work is what I'm most familiar with, because my own area is in program analysis. It would be fair to call this particular project the first actually workable software model checker. It laid the groundwork for another important project from Berkeley, BLAST, and some followup work from MSR Bangalore, Yogi.
I mean, looking at the PLDI '09 schedule, there are 6 papers co-authored by someone from MSR. Only one is primarily MSR, but another has an MSR person as first author. Looks like POPL '09 had 10 papers with at least one co-author from MSR; 7 with MSR as primary author (and 3 or so with only MSR authors).
The "cool gadgets" face of MSR is a pretty small part of it.
This is true; from a "does MSR's stuff see the market" point of view, they aren't great. But this is the same with research in general... how much CS research from even the top universities see the light of day in terms of products?
I mean, definitely some does, but not a whole lot. And what does usually takes a LONG time to show up.
Looks like Microsoft is actually starting to get serious about research...
"Starting to"? MSR is one of the biggest single contributors to CS research out there, and has been for a long time.
(Note that MSR is almost entirely distinct from what I typically call MS Corporate, which would include things like product research. Sometimes there will be something that moves from MSR to Corporate, like the SLAM work moving into the Static Driver Verifier, but MSR is still quite autonomous.)
That might make an incentive for folks to stop using so much.
I'm sure all those people who live in $CITY_WITH_DATA_CENTER and have no decision-making abilities there, but would still be affected by rising prices, would get right on that.
The economy was cruising on the downslope after the internet bubble burst in mid-2000. That happened on Clinton's watch.
It hasn't been great since 2000, but it wasn't terrible either. From the high in 2000 to the low in 2003, the Dow was down about 1/3. Both the peak at the high and the valley at the low were pretty short-lived, and saying it dropped 1/4 wouldn't be unreasonable.
Compare this to the recent drop; from the high in 2007 to the low in 2008, the Dow dropped by about 55%, a full 20% more than the drop 2000-2003. Smoothing out the peak and valley, I'd say a drop from 13500-8000 would be reasonable to count, but that's a 40% drop, still more than the peak-to-peak drop of the dot-com bust.
As a final metric, look at total change in the Dow for the time period in office. Counting inauguration->inauguration, the Dow went up about 240% under Clinton, and up about 12% for Bush. Even being almost as mean as possible for Clinton and counting the dot-com bust as the fault of his administration and counting to the 2003 low, it still more than doubled. (By contrast, being as mean as possible for Bush gives him a loss of about 1/3 under his presidency.)
The differences are quite drastic.
(This isn't to say it's just Clinton's fault/credit that it went up so much under him. Bush senior saw the Dow roughly double under his presidency. Reagan saw it go up by about 150%. Before that you have to go back to Eisenhower to see a large increase (again, about doubling under his presidency). At the same time, it seems pretty hard to me to argue that Clinton mismanaged the economy.)
Personally, I view "do whatever feels good at the moment and screw any consequences later" as being a general strategy of people in charge -- environmental laws, reducing regulatory rules, and such are examples in my mind of this philosophy being evidenced by conservatives, and the common business practice of preferring short-term profits in a more general sense -- so I think you attributing that as a liberal philosophy is BS.
GH3 actually.;-) GH2 had "Crazy on You". (I know this because (1) Crazy on You starts out with a really cool and fun opening riff, and (2) for a while Barracuda was the only song in the first few sets that I couldn't 5-star.
Slashdot Mirror
Exactly. But the problems go beyond that. For instance, I gave a speech on the Pledge of Allegiance. Imagine if it were a paper. How am I supposed to write this? Say "The Pledge of Allegiance is a statement that the speaker promises allegiance both to the US flag and the US itself, states that the US is a single nation beneath a diety, and that it offers liberty and fairness to all"? Then what? "The original form of the pldege, passed in 1892, only had the speaker promising allegiance to the flag and to the US, a single nation that offers liberty and fairness to all."?
I'm going to go out on a limb and say that I don't think you can write a decent paper without quoting. There are occasional exceptions; research papers (as in the "getting published in a journal/conference" sense of "research") often don't have quotes, though often have a lot of self semi-plagiarism.
If that's the case, then why don't they use a BSD-like license? Because that's all they will have if copyrights are eliminated -- anyone can take FSF code, modify it, and lock away their modifications.
In such a world, the "locking away" would be through technical, not legal, means. If someone did that, you could still reverse engineer their software, distribute their software, etc., but this wouldn't be possible today with the BSD license.
It's actually from The Open Directory (DMOZ).
The GPL does depend on copyright, but they are using it as a means to an end in some sense. They would rather have software copyrights abolished entirely than keep the GPL around.
So saying that the FSF has an "open and virulent bias against copyrights" clearly demonstrates either a lack of research, a lack of understanding, or a lack of honesty on the part of the RIAA's lawyers.
I'd say your comment illustrates one of those things on your part; the RIAA's description in that part is actually pretty accurate.
"quoting is not allowed for the papers that I turn in,"
WTF? What sort of crap school do you go to?
(Alternately, what are schools becoming?)
That's why I plan on never graduating. ;-)
(/me is a 3rd year grad student)
Burn fuel != burn as much fuel. They should be able to be made more efficient than probably anything else out there on a per-person, per-mile basis. I don't know how they stack up now though, but I would bet they're better than driving.
This causes very, very frequent delays for passengers. Enough so that many won't take the train.
It's basically stopped me.
My last Amtrak experience was a big pain. I was going from Chicago -> Pittsburgh, then catching another train from Pittsburgh. There was a freight derailment east of Chicago that basically shut down Amtrak traffic entirely, so Amtrak had to put together busing for us around the derailment. So we bussed from Chicago to Toledo, then got onto the train. At that point, if we had made it to Pittsburgh in the amount of time it was supposed to take, I *might* have been able to make the connection. We would have been coming in around 1 1/2 hours after the connection was supposed to leave, and on an earlier train ride a guy said he had ridden the train a lot, and had often seen Amtrak delay that train by an hour or two so people would make their connections. For about half of the Toledo->Pittsburgh distance, it actually looked like we'd make it... but then we sat outside of Cincinatti, not moving for over an hour. I strongly suspect that it was freights that were delaying us. By the time we got moving, there was basically no hope, and of course the train had left by the time we arrived. So basically, even though it was the fault of the freights that we were put in that situation in the first place, they still cost me a missed connection. (At that point, rather than bus for a couple more hours I just had them refund that part of my ticket, which they did no questions asked.)
I was actually moderately impressed with the way Amtrak handled what they were given; with a couple somewhat minor exceptions, there were actually mostly on the ball. (We got out of Chicago an hour late. The main problem there was that while we were actually mostly on the buses at the scheduled departure time, we then sat around for an hour waiting for some paperwork stuff apparently. Did that cost me the connection too? Very possibly.) Certainly miles better than most US airlines would have been. ("Not our fault; you're on your own until our next flight tomorrow.")
(You did forget the other main legitimate complaint -- it's slow. It's often as fast or faster to drive. When I went home by train, because of the way things work out it was about 24 hours to go by combination bus/train; driving would have been ~12 hours.)
For those of you, like me, that read TFA and the article linked from TFA and still don't know what Phorm is other than it's something that some UK ISPs are implementing and there appear to be privacy concerns, Wikipedia.
In short, it's system for doing targeted advertising by deep-packet inspection.
RAID isn't replication, and it isn't backups. SCSI is just an interface for talking to disks. You really need something at a higher level to be able to get true replication. Backups can be it, but you need to be sure that you get a consistent image of the DB. If you just naively copy bytes, it's very easy to not get this. If you just naively lock the file while you back up, you kill Exchange. Doing something that isn't one of those things either needs COW support from the OS or it needs cooperation from the actual application (Exchange).
And yes, there are XP APIs that Firefox uses that are not present on 2k,
Just out of curiosity, what sorts of stuff?
Just to counter the other reply, I would say that I, all of my friends, and most of the people who I've heard opinions of second-hand have said it's just a great game. Personally, I felt largely the same sort of "wow, this is really cool" feeling I got when playing Portal. (Not quite the same because I didn't get the same sense of "this would be really cool to do in real life" or anything like that, just from a gameplay sense.)
(And the soundtrack is not an integral part of the game from a gameplay sense, but it is great from a ambiance sense, and the way it works into the time mechanic is just really well done.)
How tied to Java is Android development? Is that the only option, or could I write in some other language if I wanted? (I don't care about C; I'm more interested in something like Python, Lisp/Scheme, and O'Caml.)
So, groundbreaking in some minor ways, but really just a continuing in the same efforts at formal proofs which have been going on for thirty or forty years now.
All research continues something that came before. "If I have seen further than others, it is because I have stood on the shoulders of giants" and all that. If you want to argue about the meaning of groundbreaking, whatever, but it's as groundbreaking as anything in software formal methods in the last couple decades.
Perhaps they are groundbreaking in that they can be applied to MSWindows 7, whereas the previous methods were more taylored to previous MS OSses (or to other OSses).
The methods they describe aren't tailored to ANY MS OS, though the implementation is. SLAM was groundbreaking because there wasn't anything that did anything even somewhat close to what it did, for any system ever.
I don't really have time to address the rest of your post now; it's late. I may get back to it tomorrow.
Maybe these tools will help generate "correct" code for some definition of correctness. But have these guys defended their choice of definition of "correctness"?
A little bit. There are two bits of how they would need to justify it: is it guaranteed to make sense, and how complete/useful it is.
The first bit is easy: the sorts of things they check for are the sorts of things that cause program or system crashes, or other clear failures. A null pointer dereference is almost always an error. Trying to lock an already-locked mutex is always an error if it's not designed to allow that. In a device driver, making a potentially-blocking function call while interrupts are disabled is always an error. (This is true on both Linux and Windows.)
The second bit, showing that proving a program is free of these errors is useful, is a little harder, because there's no program- or driver-specific behavior they can check. They can't figure out that, for instance, a program would produce incorrect output. If a calculator says that 1+1 is 3, SLAM wouldn't be able to tell you that is wrong. This problem is mitigated somewhat by the fact that SLAM takes as input a specification of the property that you want to prove, so if you DO have an application-specific check you want to make, there's a chance you could express it as something SLAM could check. No guarantee however.
At the same time, how many people around /. do you see complaining about Windows blue screens? Even now that they are relatively rare (I haven't seen one in ages despite running Windows on two computers I use regularly), crashes still spur complaints. So I would argue that yes, the definition of "correctness" they use IS useful in its own right.
And I wouldn't be alone; this is basically the current state of program analysis. Proving that a program actually does what it is supposed to is generally seen as out of reach, at least for now. (I would argue that it will be in the future too. For most programs, specifying what it means for a program to actually do what it is supposed to would require a specification on the same complexity order as the code itself. What's a formula that describes what Word is supposed to do? Or Emacs? Or Firefox?) There are tons and tons of papers out there that use some measure of correctness comparable to what the SLAM project used. One example that comes to mind is some stuff on concolic execution that came out of Lucent Labs and UIUC (Dart and the followup work Cute) that uses a definition of correct that includes things like null-pointer dereferences, divisions by zero, or the program reaching an assert statement. Again, there's no application-specific behavior that it knows about (unless you encode it in the program itself in an assert; presumably SLAM could pick this up too). But there are many other examples.
Is the application field a niche field, or will it help with OSses and general end-user applications?
How much it will help is still up in the air. Right now all of the verification methods out there are limited to very small programs. (This is the primary reason that the SLAM project targeted device drivers -- they tend to be very small.) So you won't be able to verify the whole OS any time soon, and you won't be able to verify anything but the smallest utilities.
But today's techniques actually DO work on device drivers. SLAM has been packaged up with the Driver Development Kit starting a bit over 2 years ago, and IIRC MS has added it to the WHQL driver certification process. I have no idea how much it actually helps in practice though. (It certainly has the potential to; most of Windows crashes are caused by third-party drivers.)
(There are other program analysis techniques that DO scale to large (millions of lines) programs. However, they are neither sound nor complete, so they aren't guaranteed to catch every bug and can also return l
but what, exactly do they contribute?
A fair amount of ground-breaking research. The SLAM project and followup work is what I'm most familiar with, because my own area is in program analysis. It would be fair to call this particular project the first actually workable software model checker. It laid the groundwork for another important project from Berkeley, BLAST, and some followup work from MSR Bangalore, Yogi.
I mean, looking at the PLDI '09 schedule, there are 6 papers co-authored by someone from MSR. Only one is primarily MSR, but another has an MSR person as first author. Looks like POPL '09 had 10 papers with at least one co-author from MSR; 7 with MSR as primary author (and 3 or so with only MSR authors).
The "cool gadgets" face of MSR is a pretty small part of it.
Link works for me.
This is true; from a "does MSR's stuff see the market" point of view, they aren't great. But this is the same with research in general... how much CS research from even the top universities see the light of day in terms of products?
I mean, definitely some does, but not a whole lot. And what does usually takes a LONG time to show up.
Looks like Microsoft is actually starting to get serious about research...
"Starting to"? MSR is one of the biggest single contributors to CS research out there, and has been for a long time.
(Note that MSR is almost entirely distinct from what I typically call MS Corporate, which would include things like product research. Sometimes there will be something that moves from MSR to Corporate, like the SLAM work moving into the Static Driver Verifier, but MSR is still quite autonomous.)
That might make an incentive for folks to stop using so much.
I'm sure all those people who live in $CITY_WITH_DATA_CENTER and have no decision-making abilities there, but would still be affected by rising prices, would get right on that.
The economy was cruising on the downslope after the internet bubble burst in mid-2000. That happened on Clinton's watch.
It hasn't been great since 2000, but it wasn't terrible either. From the high in 2000 to the low in 2003, the Dow was down about 1/3. Both the peak at the high and the valley at the low were pretty short-lived, and saying it dropped 1/4 wouldn't be unreasonable.
Compare this to the recent drop; from the high in 2007 to the low in 2008, the Dow dropped by about 55%, a full 20% more than the drop 2000-2003. Smoothing out the peak and valley, I'd say a drop from 13500-8000 would be reasonable to count, but that's a 40% drop, still more than the peak-to-peak drop of the dot-com bust.
As a final metric, look at total change in the Dow for the time period in office. Counting inauguration->inauguration, the Dow went up about 240% under Clinton, and up about 12% for Bush. Even being almost as mean as possible for Clinton and counting the dot-com bust as the fault of his administration and counting to the 2003 low, it still more than doubled. (By contrast, being as mean as possible for Bush gives him a loss of about 1/3 under his presidency.)
The differences are quite drastic.
(This isn't to say it's just Clinton's fault/credit that it went up so much under him. Bush senior saw the Dow roughly double under his presidency. Reagan saw it go up by about 150%. Before that you have to go back to Eisenhower to see a large increase (again, about doubling under his presidency). At the same time, it seems pretty hard to me to argue that Clinton mismanaged the economy.)
Personally, I view "do whatever feels good at the moment and screw any consequences later" as being a general strategy of people in charge -- environmental laws, reducing regulatory rules, and such are examples in my mind of this philosophy being evidenced by conservatives, and the common business practice of preferring short-term profits in a more general sense -- so I think you attributing that as a liberal philosophy is BS.
It is Clinton all over again. Hang on to your wallets!
Because... the economy did so badly under Clinton?
GH3 actually. ;-) GH2 had "Crazy on You". (I know this because (1) Crazy on You starts out with a really cool and fun opening riff, and (2) for a while Barracuda was the only song in the first few sets that I couldn't 5-star.