Simplistic, you mean. Repeat after me: The grid is not a battery. Yes, you may be able to sell some excess power to the "grid", but the "grid" doesn't store energy, it just distributes it. You can't buy "your" power back again.
So to repeat, a power station connected to the grid still needs to be able to supply ALL of the energy everyone needs at home on a cold night.
Fortunately, the amount of power needed at night is far lower than that needed during the day. Other power generation mechanisms are sufficient for these levels. If you want to go all-renewable, wind could provide the left over power needed at night.
I can see solar as a potential option for some businesses, but for home use you still have the small problem of no power output during the night. And that's usually just when you want some lights, television, heat, and so forth.
If they want solar to REALLY catch on someone is going to need to develop not just a cost-effective solar cell, but also a cost-effective way to store and reuse the energy collected during the day.
This is a non-issue. The technology and legislation addressing this has existed for nearly a decade: feed power back into the grid. You sell power to the power company when generating, and you buy it back when you're not generating. Simple.
Funny how everytime solar comes up anywhere, someone trumpets out this "problem". Come on people, do you honestly think such a trivial problem would go unsolved for so long?
Re: money saved with solar does not break even
Numerous studies have demonstrated that the payback for solar is anywhere from 2 to 10 years (depending on circumstances such as location). Solar cells last 10 to 20 years. You do the math.
That's where a project like LLVM comes in. Platform-neutral binaries via LLVM bytecode, and full processor-specific link-time native compilation+optimization when a binary is installed. Alternatively, you can JIT the bytecode at runtime. Developers just distribute LLVM bytecode binaries, and the installers/users do the rest. I think the LLVM approach is the future.
It would make the namespace a lot less cluttered and would reduce trademark abuses. On the other hand, names would be a lot longer. However, if you're using a search engine, a portal or bookmarks most of the time anyway, that's no big deal.
If you're going to use bookmarks, portals and search engines anyway, why not leverage them fully and make all names/identifiers collision-free cryptographic names. Trademark problem: solved permanently.
Googles anti-phising filter (as in google toolbar) is the one who is constantly sending your HTTP requests to Googles servers. There was a slashdot post about this a while ago, but I cannot find it.
Actually, it's horrible. It submits every URL you try to access to MS for verification. Same with the Google toolbar in fact, except the latter is even worse because it submits it over an unencrypted connection. These anti-phishing efforts break the current semantics of the web. These efforts are seriously misguided and truly disheartening, particularly when there are perfectly good anti-phishing tools that do things right.
Lying requires more brain horsepower than telling the truth and the parts of the brain used for lying are known. They are different than just recall.
What if you've rehearsed and memorized your cover story so you're just recalling your lie? How can this situation be distinguished from recalling a true memory?
Here is honestly the scariest thing I've read recently:
The fight between Dr. Hansen and administration officials echoes other recent disputes. At climate laboratories of the National Oceanic and Atmospheric Administration, for example, many scientists who routinely took calls from reporters five years ago can now do so only if the interview is approved by administration officials in Washington, and then only if a public affairs officer is present or on the phone.
Yes, I was referring to the speed of light in a vacuum, as this is generally understood when dealing with this particular subject matter. I further concur with and heartily recommend scepticism, but the original post was making incomplete claims of Relativity, so I just had to correct them. The metaphysics of the true nature of reality is probably best left to forums like infidels.:-)
No no, the GP is correct. When you're talking about the speed of light, 'c', you're talking about the speed of light in a vacuum.
I never took issue with light being slowed, I took issue only with the statement I quoted. The laws of physics are the same in all frames of reference. The GP was incorrect in this statement, and I corrected him/her.
Gravity also can have an effect on the speed of light.
No, it has an effect on the frequency of light, not the speed.
The speed of light in vacuum is the same in all frames of reference.
The general axiom is that the laws of physics are the same in all frames of reference (the very heart of "relativity"). The speed of light is merely an inference from this general rule.
The very word, RELATIVITY, indicates the complexity and the depth that must be considered when working with the laws of physics. The laws can change and DO change relative to where you are and how fast you are moving and any number of other factors.
Actually, one of the fundamental axioms of relativity is that the laws of physics are the same in all frames of reference. This is why the speed of light is the same in all frames of reference.
Read elsewhere in this thread for the actual published paper, read it, and you'll see why. Converting photons to gravito-photons relies on particular conditions (due to the nature of the gravitational-electromagnetic linkage) [1]. Further, continuous magnetic fields, not pulsed fields, might be necessary [2].
I know we need DNS today -- links, bookmarks, advertising, all that.
Bookmarks and links are a technology which actually eliminate the need for DNS[1]. If you could pass bookmarks and links around in a user-friendly manner, why would you need a global namespace like DNS? The links could simply be IP addresses, or preferably, a cryptographic identifier [2],[6]. Finding an entity with an introduction occurs via a e-mail, links on the web, etc. Search engines are used for finding an entity without an introduction (like the Yellow pages) [3],[4].
All the technologies to replace DNS exist today. They aren't quite as easy to use as DNS, given that software hasn't been designed to use them in this fashion, but the DNS is an unnecessary, vulnerable, centralized system, even today.
The technologies I've pointed out further solve the phishing problem, enable secure introduction, and decentralized secure computation.
The problem with your self-made whitelist situation is that you have no way to authenticate your bank's website the first time.
You have just as much assurance on the first load as you do with the current system with a CA-issued cert. The critical difference, is that thenceforth you have perfect assurance with Petnames that you are dealing with the same entity as you were originally. You don't have that guarantee with CAs.
Does it really matter how many C's preceded the first C? Furthermore if you cut it anywhere after the second statement you're left with the same question, "Why did C occur?". So this provides no extra value to the argument. Why are the C's in an infinite sequence? Why did it suddenly (and apparently randomly) break away from repeating C's to cause B? Could it be that all those C's aren't really C's, but actually differ? If so what was the first instance that started it?
Right, this makes sense. And yet there are still two problems:
What if A and B are in a constant causal loop. There is no logical inconsistency here is there? If so, then a causal loop of arbitrary length is also consistent. A causes B causes C causes... causes A... ad infinitum.
A cause can have more than one effect, while an effect has only one cause.
This is important, because I have logical "proofs of God" which are predicated on the assumptions that an infinite regression of causes is impossible. Hatcher never explained why in his lecture however, and I can't think of why the universe couldn't logically have existed forever (ignoring physical reasons such as thermodynamics for the moment -- it could simply be a case of ignorance of the mechanism involved in reducing entropy).
Eliminating infinite regressions forces one to acknowledge a moment of creation. A moment of creation implies a creative element of some kind G as described in the proof (which Hatcher calls God). So I'm trying to understand whether the assumption on avoiding infinite regressions is valid.
It's also open to an infinite regression, which, just as in coding, is a sure sign that there is something wrong with your logic.
I really don't understand the problem with infinite regressions. For instance, what is the inherent logical inconcistency with having an infinite regression of causes? Infinity as a concept is perfectly logical (whole numbers are countably infinite).
The above implies that you know, so perhaps you can spell it out for me. I've seen many arguments avoiding infinite regression of causes, but never any explanation as to why it's necessary. Inquiring minds would like to know.
That's rich, coming from someone who has repeatedly been caught making false statements and won't even admit it.
I openly admit to anything I said that was false. Singularity is indeed a single-address space OS; I misread a section dealing with virtual memory and processes which led me to conclude it wasn't. That's a far cry from being a liar. But hey, you go on thinking the worst of people. Good luck with that.
You corrected me on the single-address space issue, I left it at that. So because I didn't bow down and lick your boots and beg your forgiveness for being wrong on a particular point that I all of a sudden "won't admit to being wrong"? That's pretty childish.
The only other point of contention were the capabilities of the verifier. We disagreed on the ability of the verifier to ensure correct "state transitions". It took you three exchanges to finally define what constitutes a "state transition", after which I agreed that the verifier could enforce "state transitions" over the external communication protocol. Unfortunately, that was not what I was originally concerned with, so here we are yet again.
I am doing no such thing. (Re: defining "algorithmic" bugs as superset of all bugs)
You just did in your parent post. I even quoted you. Really, your memory can't be that short.
You're the one who first referred to "algorithmic bugs" so why don't you define it?
I just did in the post you replied to. I even alluded to it, if somewhat imprecisely, in my original post.
Until you do, I'll assume the intuitive meaning of bugs that represent high-level logic errors (e.g. deadlock/livelock, indefinite postponement, race conditions) as opposed to low-level implementation artifacts (e.g. incrementing the wrong variable, fencepost errors).
In an abstract sense, an error is a state transition that the programmer did not intend in attempting to achieve his goals (either the algorithm itself was incorrect, or the algorithm was not implemented correctly). The class of errors I alluded to earlier, are those invalid state transitions which are internal to the core portion of an application (such as the HTTP request parser in a web server). The class of errors the verifier eliminates, are the state transitions associated with communicating with external entities. I'm not sure how you can possibly classify the two as synonymous, or one the subset of the other (as you did in your previous post). The two are quite clearly disjoint, and any intersection is coincidental (for those objects whose logic is merely communication itself -- such as a socket).
Dispatching to the wrong handler will often lead to generation of an invalid response, which can very much be caught by a verifier.
That's plain ridiculous. You are directly correlating internal state with external communication behaviour. There is sometimes strong correlation, but it is by no means guaranteed. If the correlation is strong, it is either due to the nature of the application (ie. a socket), or by coincidence. Coincidence is not a programming tool particularly for a reliable system.
In the HTTP example, errors and success are both transmitted in an identical fashion. There is no distinction observable to the Singularity verifier. It is always texty request-texty response.
This is less apparent in HTTP than in other protocols because HTTP was designed by an amateur,
Ok, if you say so... Regardless, this problem is inherent to ALL texty or serialized protocols. SMTP, POP3, any byte-stream protocol really. The verifier cannot check any of these natively.
Even if that weren't the case, the fact that there's one error a verifier could not detect in no way proves your claim that a verifier can do nothing. You still seem to be struggling with that distinction between "not every" and "none" don't you?
Firstly, we are not discussing "a verifier", we are discussing the "Singularity verifier". I fully acknowledge that some future
The idea is that all applications running on the operating system (including their IPC) are either provably correct or bounded at run time.
This is simply impossible. The Halting Problem demonstrates that it's impossible to construct a general algorithm that can determine whether some other general algorithm will halt (unless this isn't what you meant by saying "applications running on the OS are [...] bounded at run time").
It's impossible to prove that applications written in Sing#/Spec#C# are correct simply because the compiler cannot divine the intentions of the programmer, and thus it cannot know what the output "should be" in order to compare it to what actually came out. Only by combining languages and proof systems can we hope to achieve this end, and Sing#/C#/Spec# are still far from that goal.
All IPC is necessarily bounded at run-time (limited by machine addressable limits), and in all microkernels the IPC data is validated to ensure that unauthorized accesses do not occur.
Hmm... perhaps you should clarify what you meant here, since there are so many interpretations.
It's important that these restraints be enforced by the operating system. By enforcing these restraints in the operating system, you guarantee that things like buffer overruns and segfauls cannot occur.
This is a language-level issue, not an operating system one.
That's why IPC must be verified by the OS: it guarantees that an application couldn't possibly corrupt some other application.
IPC is always verified in every operating system. But IPC itself is not what causes buffer overflows or security breaches.
If these things were done using a VM in userspace (Java?) then the security and reliability holes would remain--as long as code verification is optional (by writing in Java rather than C), the malicious coder will opt not to use it.
I think the growing developer base for Java and.Net say otherwise. If verification exists, and it makes your programs more correct simply by turning it on, why wouldn't people use it?
Also, the isolation enforced by code verification is much more stringent than the isolation enforced by an MMU.
This is true. It remains to be seen whether it is practical however.
Also, the isolation enforced by code verification is much more stringent than the isolation enforced by an MMU.
Yes, but you are thinking of course-grained process-level operating systems like Linux. Operating systems built on microkernels offer much finer process granularity since their performance is so much higher. Files, directories, even sockets are all implemented as processes on EROS.
In addition, enforcing isolation through code verification does not impose the same run-time performance penalties as MMUs, which thus far have limited the adoption of microkernels.
True. Unfortunately, a compiler which can provide this sophisticated analysis is not here yet, or if it is, it clearly has some disadvantages in other areas (perhaps performance?).
Either you're the stupidest person on Slashdot (quite an achievement) or you're playing dumb to red herring to distract from your previous dishonesty. [...] Protocols are actually all around you, and only your own narrowness of vision prevents you from seeing that.
Ad-hominem attacks do not add credibility to your arguments FYI. And as I said earlier, please avoid trying to divine my state of mind; you know nothing about me, and every personal attack you make and every strawman you propose just makes you look more ignorant and childish. You can presume I'm deliberately antagonizing you or you can presume that we're having a strictly intellectual disagreement or perhaps a misunderstanding. Personally, I prefer to stick to the facts. Your call. That's the last I'll say on the matter.
Wrong again. It cannot catch all of these sorts of bugs, and nobody has said that it could. [...] Your statement, though, was that a verifier can do nothing about such bugs.
Which bugs are "such bugs"? You are classifying "algorithmic" bugs as the superset of all types of bugs ("I'll reduce it to purely logical terms. Let X be the set of algorithmic errors, Y the subset of protocol errors"). In the Church-Turing sense of "algorithm" word your use might be correct (although some people disagree), but you're completely ignoring the constraints I placed on my original, specific use of the word. The verifier ensures the correct sequence of requests/responses via endpoints, but it says nothing about the application's internal state.
You can accuse me of "moving the goal posts" all you like, but that statement is perfectly consistent with every statement I've made then and since. That statement is still true. Now that we've agreed on what was meant by "state transitions" (ie. being specific to the protocol state machine), it is largely orthogonal to my original concerns. Or as you would say, X (my constrained "algorithmic" bugs) and Y (protocol bugs) are disjoint sets.
Returning to my original example, a web server which incorrectly dispatches to a POST handler on a GET request has performed an invalid application state transition, even though the protocol state transition was valid. My original statement, stands: the verifier can do nothing about this sort of bug. You seem to be having difficulty understanding that right from the outset we weren't quite on the same page. Hence why I asked you to define "state transition". Then you accuse me of "moving the goalposts", instead of assuming that perhaps we were talking at cross-purposes. Really, try being less hostile and adversarial in the future.
An external protocol is, quite obviously, one that is used to communicate with an external entity - i.e. on another box, running a different OS image, accessed via an external network interface.
But this distinction does not exist in the software world; there are no "external" entities, merely interfaces to "other objects". These objects can be local or remote, they can be devices, etc. Yes, everything you point out is a "protocol", and yet, you called HTTP an "external" protocol. So what distinguishes an "external" protocol from an "internal" one? Are you drawing a distinction between a "native" protocol, such as a function calling convention, and one that must be "interpreted" and is thus "non-native"? Is this the distinction you're drawing between HTTP and the native, verifiable protocol in Sing#? It's a simple question.
There is no reason why two objects on the same machine or even in the same address space cannot communicate via HTTP (and they commonly do for web services in the former case), so you're "external protocol" distinction does not make sense.
It's selective in the sense of argument by selective observation. I realize you're not fluent in English, but please at least try to understand people before you disagree with them.
So unless the verifier can catch all algorithmic errors, it's worthless? Bullshit.
I never said any such thing. Slashdot posters are really big fans of the strawman aren't they? Word of advice, before replying, take a deep breath, relax, and read carefully.
What is meant by protocol error is also quite clear from the paper - it's a protocol between components in the system (not one handled externally like HTTP) expressed as state transitions forming a channel contract. It really is right in there. It's what distinguishes Sing# from Spec#. The verifier can catch those errors, and the fact that it's a subset of all algorithmic errors is a red herring. Your statement remains false.
No, it really doesn't. Let's review. Here is the original statement I made which you disagreed with:
From the application perspective, if it contains an algorithmic error, the state transition may trigger a bug, so a message may induce an incorrect state transition. There is nothing a verifier can do to prevent this.
This statement is predicated on a particular definition of "state transition". This is why I asked for your definition of "state transition" to compare to mine, and why I qualified it from different perspectives (application, kernel, etc.). The original statement stands: an application can indeed be left in an "invalid state" following a communication and the verifier cannot catch these sorts of bugs. In fact, immediately following that original statement I clarified:
Only a system programmed fully with verification proofs can make guarantees about total correctness in the face of changing state.
Yet, you quoted the original statement in "bad faith" ignoring this clarification which makes it quite clear where I'm coming from. So instead of answering the question and fruitfully advancing this discussion, you chose to attack a strawman.
So, now we're getting somewhere: what the verifier does buy you, is that the message input and output sequence is explicitly enumerated and the verifier ensures that the exit points of the code dispatched on these messages return the expected reply message types. Right?
Finally, perhaps you can clarify what you mean by HTTP being an "external protocol". Do you only mean that it does not use the platform's built-in protocol mechanisms? Hate to break it to you, but most of the world is composed of protocols of this nature.
You said type and memory safety were the only guarantees. Key word: only.
Because I did not see the relevance of "protocol" to "algorithmic correctness" as I was arguing it.
...and that doesn't count because...? Oh, because it's not convenient for you. Because disavowing it, however speciously, gives you an opportunity to play "I'm rubber, you're glue" games. Grow up.
I didn't bring EROS up, I merely corrected an error. Once corrected, I did not drag EROS into anything. You are dragging it in now. Really, it's not that hard to understand.
Quoting a source in good faith is a good thing. Selectively quoting or misquoting is not. Clear enough?
Should I have quoted the entire paper? I'm sure you agree that every quote is a selective quote. I copied and pasted the text verbatim from the paper, so I didn't misquote. Please, clarify exactly what about my quote was in "bad faith".
Slashdot Mirror
I really don't think selling hybrids is an issue. There is a waiting list for the Toyota Prius here in Toronto.
Simplistic, you mean. Repeat after me: The grid is not a battery. Yes, you may be able to sell some excess power to the "grid", but the "grid" doesn't store energy, it just distributes it. You can't buy "your" power back again.
So to repeat, a power station connected to the grid still needs to be able to supply ALL of the energy everyone needs at home on a cold night.
Fortunately, the amount of power needed at night is far lower than that needed during the day. Other power generation mechanisms are sufficient for these levels. If you want to go all-renewable, wind could provide the left over power needed at night.
I can see solar as a potential option for some businesses, but for home use you still have the small problem of no power output during the night. And that's usually just when you want some lights, television, heat, and so forth.
If they want solar to REALLY catch on someone is going to need to develop not just a cost-effective solar cell, but also a cost-effective way to store and reuse the energy collected during the day.
This is a non-issue. The technology and legislation addressing this has existed for nearly a decade: feed power back into the grid. You sell power to the power company when generating, and you buy it back when you're not generating. Simple.
Funny how everytime solar comes up anywhere, someone trumpets out this "problem". Come on people, do you honestly think such a trivial problem would go unsolved for so long?
Re: money saved with solar does not break even
Numerous studies have demonstrated that the payback for solar is anywhere from 2 to 10 years (depending on circumstances such as location). Solar cells last 10 to 20 years. You do the math.
That's where a project like LLVM comes in. Platform-neutral binaries via LLVM bytecode, and full processor-specific link-time native compilation+optimization when a binary is installed. Alternatively, you can JIT the bytecode at runtime. Developers just distribute LLVM bytecode binaries, and the installers/users do the rest. I think the LLVM approach is the future.
It would make the namespace a lot less cluttered and would reduce trademark abuses. On the other hand, names would be a lot longer. However, if you're using a search engine, a portal or bookmarks most of the time anyway, that's no big deal.
If you're going to use bookmarks, portals and search engines anyway, why not leverage them fully and make all names/identifiers collision-free cryptographic names. Trademark problem: solved permanently.
Slashdot had an article on a "hyperdrive" paper which is based upon Heim Theory. Heim theory postulates EM-gravity coupling via the gravito-photon, and the experiment the Heim researchers recommended to produce gravito-photons, and thus produce gravitational effects, sounds similar to what this article is describing.
Googles anti-phising filter (as in google toolbar) is the one who is constantly sending your HTTP requests to Googles servers. There was a slashdot post about this a while ago, but I cannot find it.
Perhaps it's my comment you're referring to.
Wow. Talk about a potential privacy issue. I wonder if that will be removed for the final release.
I doubt it. That's how it's intended to operate.
Built-in phishing protection = good
Actually, it's horrible. It submits every URL you try to access to MS for verification. Same with the Google toolbar in fact, except the latter is even worse because it submits it over an unencrypted connection. These anti-phishing efforts break the current semantics of the web. These efforts are seriously misguided and truly disheartening, particularly when there are perfectly good anti-phishing tools that do things right.
Lying requires more brain horsepower than telling the truth and the parts of the brain used for lying are known. They are different than just recall.
What if you've rehearsed and memorized your cover story so you're just recalling your lie? How can this situation be distinguished from recalling a true memory?
and even then, peoples perceptions of the "early days" are more often than not incorrect.
This is Francis Bacon's "Idol of the Den" (Idola Specus). It is a recognized form of human bias, specific to the individual. See the above link, or this one higher in the thread for a description of the four fundamental types of human bias.
Yes, I was referring to the speed of light in a vacuum, as this is generally understood when dealing with this particular subject matter. I further concur with and heartily recommend scepticism, but the original post was making incomplete claims of Relativity, so I just had to correct them. The metaphysics of the true nature of reality is probably best left to forums like infidels. :-)
No no, the GP is correct. When you're talking about the speed of light, 'c', you're talking about the speed of light in a vacuum.
I never took issue with light being slowed, I took issue only with the statement I quoted. The laws of physics are the same in all frames of reference. The GP was incorrect in this statement, and I corrected him/her.
Gravity also can have an effect on the speed of light.
No, it has an effect on the frequency of light, not the speed.
The speed of light in vacuum is the same in all frames of reference.
The general axiom is that the laws of physics are the same in all frames of reference (the very heart of "relativity"). The speed of light is merely an inference from this general rule.
The very word, RELATIVITY, indicates the complexity and the depth that must be considered when working with the laws of physics. The laws can change and DO change relative to where you are and how fast you are moving and any number of other factors.
Actually, one of the fundamental axioms of relativity is that the laws of physics are the same in all frames of reference. This is why the speed of light is the same in all frames of reference.
Read elsewhere in this thread for the actual published paper, read it, and you'll see why. Converting photons to gravito-photons relies on particular conditions (due to the nature of the gravitational-electromagnetic linkage) [1]. Further, continuous magnetic fields, not pulsed fields, might be necessary [2].
I AA2005-4321Letter.pdf
[1] http://en.wikipedia.org/wiki/Heim_Theory
[2] http://www.hpcc-space.de/publications/documents/A
I know we need DNS today -- links, bookmarks, advertising, all that.
a mes.html (Petnames are a sort-of local DNS directory)b ruary/002891.htmlb ruary/003079.html
Bookmarks and links are a technology which actually eliminate the need for DNS[1]. If you could pass bookmarks and links around in a user-friendly manner, why would you need a global namespace like DNS? The links could simply be IP addresses, or preferably, a cryptographic identifier [2],[6]. Finding an entity with an introduction occurs via a e-mail, links on the web, etc. Search engines are used for finding an entity without an introduction (like the Yellow pages) [3],[4].
All the technologies to replace DNS exist today. They aren't quite as easy to use as DNS, given that software hasn't been designed to use them in this fashion, but the DNS is an unnecessary, vulnerable, centralized system, even today.
The technologies I've pointed out further solve the phishing problem, enable secure introduction, and decentralized secure computation.
[1] http://www.skyhunter.com/marcs/petnames/IntroPetN
[2] http://yurl.net/ (a YURL redirectory is pretty much like DNS, except that anyone can set one up)
[3] http://www.eros-os.org/pipermail/cap-talk/2005-Fe
[4] http://www.eros-os.org/pipermail/cap-talk/2005-Fe
[5] http://petname.mozdev.org/
web-calculus and the waterken server, Freenet, L4 microkernel, EROS microkernel (in fact, a great deal of computer science research is open source).
The problem with your self-made whitelist situation is that you have no way to authenticate your bank's website the first time.
You have just as much assurance on the first load as you do with the current system with a CA-issued cert. The critical difference, is that thenceforth you have perfect assurance with Petnames that you are dealing with the same entity as you were originally. You don't have that guarantee with CAs.
Right, this makes sense. And yet there are still two problems:
This is important, because I have logical "proofs of God" which are predicated on the assumptions that an infinite regression of causes is impossible. Hatcher never explained why in his lecture however, and I can't think of why the universe couldn't logically have existed forever (ignoring physical reasons such as thermodynamics for the moment -- it could simply be a case of ignorance of the mechanism involved in reducing entropy).
Eliminating infinite regressions forces one to acknowledge a moment of creation. A moment of creation implies a creative element of some kind G as described in the proof (which Hatcher calls God). So I'm trying to understand whether the assumption on avoiding infinite regressions is valid.
It's also open to an infinite regression, which, just as in coding, is a sure sign that there is something wrong with your logic.
I really don't understand the problem with infinite regressions. For instance, what is the inherent logical inconcistency with having an infinite regression of causes? Infinity as a concept is perfectly logical (whole numbers are countably infinite).
The above implies that you know, so perhaps you can spell it out for me. I've seen many arguments avoiding infinite regression of causes, but never any explanation as to why it's necessary. Inquiring minds would like to know.
That's rich, coming from someone who has repeatedly been caught making false statements and won't even admit it.
I openly admit to anything I said that was false. Singularity is indeed a single-address space OS; I misread a section dealing with virtual memory and processes which led me to conclude it wasn't. That's a far cry from being a liar. But hey, you go on thinking the worst of people. Good luck with that.
You corrected me on the single-address space issue, I left it at that. So because I didn't bow down and lick your boots and beg your forgiveness for being wrong on a particular point that I all of a sudden "won't admit to being wrong"? That's pretty childish.
The only other point of contention were the capabilities of the verifier. We disagreed on the ability of the verifier to ensure correct "state transitions". It took you three exchanges to finally define what constitutes a "state transition", after which I agreed that the verifier could enforce "state transitions" over the external communication protocol. Unfortunately, that was not what I was originally concerned with, so here we are yet again.
I am doing no such thing. (Re: defining "algorithmic" bugs as superset of all bugs)
You just did in your parent post. I even quoted you. Really, your memory can't be that short.
You're the one who first referred to "algorithmic bugs" so why don't you define it?
I just did in the post you replied to. I even alluded to it, if somewhat imprecisely, in my original post.
Until you do, I'll assume the intuitive meaning of bugs that represent high-level logic errors (e.g. deadlock/livelock, indefinite postponement, race conditions) as opposed to low-level implementation artifacts (e.g. incrementing the wrong variable, fencepost errors).
In an abstract sense, an error is a state transition that the programmer did not intend in attempting to achieve his goals (either the algorithm itself was incorrect, or the algorithm was not implemented correctly). The class of errors I alluded to earlier, are those invalid state transitions which are internal to the core portion of an application (such as the HTTP request parser in a web server). The class of errors the verifier eliminates, are the state transitions associated with communicating with external entities. I'm not sure how you can possibly classify the two as synonymous, or one the subset of the other (as you did in your previous post). The two are quite clearly disjoint, and any intersection is coincidental (for those objects whose logic is merely communication itself -- such as a socket).
Dispatching to the wrong handler will often lead to generation of an invalid response, which can very much be caught by a verifier.
That's plain ridiculous. You are directly correlating internal state with external communication behaviour. There is sometimes strong correlation, but it is by no means guaranteed. If the correlation is strong, it is either due to the nature of the application (ie. a socket), or by coincidence. Coincidence is not a programming tool particularly for a reliable system.
In the HTTP example, errors and success are both transmitted in an identical fashion. There is no distinction observable to the Singularity verifier. It is always texty request-texty response.
This is less apparent in HTTP than in other protocols because HTTP was designed by an amateur,
Ok, if you say so... Regardless, this problem is inherent to ALL texty or serialized protocols. SMTP, POP3, any byte-stream protocol really. The verifier cannot check any of these natively.
Even if that weren't the case, the fact that there's one error a verifier could not detect in no way proves your claim that a verifier can do nothing. You still seem to be struggling with that distinction between "not every" and "none" don't you?
Firstly, we are not discussing "a verifier", we are discussing the "Singularity verifier". I fully acknowledge that some future
Hmm... perhaps you should clarify what you meant here, since there are so many interpretations.
It's important that these restraints be enforced by the operating system. By enforcing these restraints in the operating system, you guarantee that things like buffer overruns and segfauls cannot occur.
This is a language-level issue, not an operating system one.
That's why IPC must be verified by the OS: it guarantees that an application couldn't possibly corrupt some other application.
IPC is always verified in every operating system. But IPC itself is not what causes buffer overflows or security breaches.
If these things were done using a VM in userspace (Java?) then the security and reliability holes would remain--as long as code verification is optional (by writing in Java rather than C), the malicious coder will opt not to use it.
I think the growing developer base for Java and
Also, the isolation enforced by code verification is much more stringent than the isolation enforced by an MMU.
This is true. It remains to be seen whether it is practical however.
Also, the isolation enforced by code verification is much more stringent than the isolation enforced by an MMU.
Yes, but you are thinking of course-grained process-level operating systems like Linux. Operating systems built on microkernels offer much finer process granularity since their performance is so much higher. Files, directories, even sockets are all implemented as processes on EROS.
In addition, enforcing isolation through code verification does not impose the same run-time performance penalties as MMUs, which thus far have limited the adoption of microkernels.
True. Unfortunately, a compiler which can provide this sophisticated analysis is not here yet, or if it is, it clearly has some disadvantages in other areas (perhaps performance?).
Either you're the stupidest person on Slashdot (quite an achievement) or you're playing dumb to red herring to distract from your previous dishonesty. [...] Protocols are actually all around you, and only your own narrowness of vision prevents you from seeing that.
Ad-hominem attacks do not add credibility to your arguments FYI. And as I said earlier, please avoid trying to divine my state of mind; you know nothing about me, and every personal attack you make and every strawman you propose just makes you look more ignorant and childish. You can presume I'm deliberately antagonizing you or you can presume that we're having a strictly intellectual disagreement or perhaps a misunderstanding. Personally, I prefer to stick to the facts. Your call. That's the last I'll say on the matter.
Wrong again. It cannot catch all of these sorts of bugs, and nobody has said that it could. [...] Your statement, though, was that a verifier can do nothing about such bugs.
Which bugs are "such bugs"? You are classifying "algorithmic" bugs as the superset of all types of bugs ("I'll reduce it to purely logical terms. Let X be the set of algorithmic errors, Y the subset of protocol errors"). In the Church-Turing sense of "algorithm" word your use might be correct (although some people disagree), but you're completely ignoring the constraints I placed on my original, specific use of the word. The verifier ensures the correct sequence of requests/responses via endpoints, but it says nothing about the application's internal state.
You can accuse me of "moving the goal posts" all you like, but that statement is perfectly consistent with every statement I've made then and since. That statement is still true. Now that we've agreed on what was meant by "state transitions" (ie. being specific to the protocol state machine), it is largely orthogonal to my original concerns. Or as you would say, X (my constrained "algorithmic" bugs) and Y (protocol bugs) are disjoint sets.
Returning to my original example, a web server which incorrectly dispatches to a POST handler on a GET request has performed an invalid application state transition, even though the protocol state transition was valid. My original statement, stands: the verifier can do nothing about this sort of bug. You seem to be having difficulty understanding that right from the outset we weren't quite on the same page. Hence why I asked you to define "state transition". Then you accuse me of "moving the goalposts", instead of assuming that perhaps we were talking at cross-purposes. Really, try being less hostile and adversarial in the future.
An external protocol is, quite obviously, one that is used to communicate with an external entity - i.e. on another box, running a different OS image, accessed via an external network interface.
But this distinction does not exist in the software world; there are no "external" entities, merely interfaces to "other objects". These objects can be local or remote, they can be devices, etc. Yes, everything you point out is a "protocol", and yet, you called HTTP an "external" protocol. So what distinguishes an "external" protocol from an "internal" one? Are you drawing a distinction between a "native" protocol, such as a function calling convention, and one that must be "interpreted" and is thus "non-native"? Is this the distinction you're drawing between HTTP and the native, verifiable protocol in Sing#? It's a simple question.
There is no reason why two objects on the same machine or even in the same address space cannot communicate via HTTP (and they commonly do for web services in the former case), so you're "external protocol" distinction does not make sense.
It's selective in the sense of argument by selective observation. I realize you're not fluent in English, but please at least try to understand people before you disagree with them.
Why would you assume I'm not fluent in English?
I never said any such thing. Slashdot posters are really big fans of the strawman aren't they? Word of advice, before replying, take a deep breath, relax, and read carefully.
What is meant by protocol error is also quite clear from the paper - it's a protocol between components in the system (not one handled externally like HTTP) expressed as state transitions forming a channel contract. It really is right in there. It's what distinguishes Sing# from Spec#. The verifier can catch those errors, and the fact that it's a subset of all algorithmic errors is a red herring. Your statement remains false.
No, it really doesn't. Let's review. Here is the original statement I made which you disagreed with:This statement is predicated on a particular definition of "state transition". This is why I asked for your definition of "state transition" to compare to mine, and why I qualified it from different perspectives (application, kernel, etc.). The original statement stands: an application can indeed be left in an "invalid state" following a communication and the verifier cannot catch these sorts of bugs. In fact, immediately following that original statement I clarified:Yet, you quoted the original statement in "bad faith" ignoring this clarification which makes it quite clear where I'm coming from. So instead of answering the question and fruitfully advancing this discussion, you chose to attack a strawman.
So, now we're getting somewhere: what the verifier does buy you, is that the message input and output sequence is explicitly enumerated and the verifier ensures that the exit points of the code dispatched on these messages return the expected reply message types. Right?
Finally, perhaps you can clarify what you mean by HTTP being an "external protocol". Do you only mean that it does not use the platform's built-in protocol mechanisms? Hate to break it to you, but most of the world is composed of protocols of this nature.
You said type and memory safety were the only guarantees. Key word: only.
Because I did not see the relevance of "protocol" to "algorithmic correctness" as I was arguing it.
I didn't bring EROS up, I merely corrected an error. Once corrected, I did not drag EROS into anything. You are dragging it in now. Really, it's not that hard to understand.
Quoting a source in good faith is a good thing. Selectively quoting or misquoting is not. Clear enough?
Should I have quoted the entire paper? I'm sure you agree that every quote is a selective quote. I copied and pasted the text verbatim from the paper, so I didn't misquote. Please, clarify exactly what about my quote was in "bad faith".