Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.arch.embedded > #27996 > unrolled thread
| Started by | pozz <pozzugno@gmail.com> |
|---|---|
| First post | 2018-09-14 09:50 +0200 |
| Last post | 2018-09-14 13:49 +0300 |
| Articles | 20 on this page of 61 — 13 participants |
Back to article view | Back to comp.arch.embedded
arm-gcc: pointer to constant string pozz <pozzugno@gmail.com> - 2018-09-14 09:50 +0200
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-14 11:18 +0200
Re: arm-gcc: pointer to constant string pozz <pozzugno@gmail.com> - 2018-09-14 13:05 +0200
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-14 13:25 +0200
Re: arm-gcc: pointer to constant string Nils M Holm <nmh@ananda.local> - 2018-09-14 09:47 +0000
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-14 12:26 +0200
Re: arm-gcc: pointer to constant string Stef <stef33d@yahooI-N-V-A-L-I-D.com.invalid> - 2018-09-14 14:52 +0200
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-14 16:04 +0200
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-14 15:48 +0100
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-14 17:02 +0200
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-14 18:45 +0100
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-14 20:37 +0200
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-14 20:51 +0100
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-15 16:24 +0200
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-15 17:28 +0100
Re: arm-gcc: pointer to constant string Clifford Heath <no.spam@please.net> - 2018-09-16 13:58 +1000
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-16 08:42 +0100
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-16 08:47 +0100
Re: arm-gcc: pointer to constant string Clifford Heath <no.spam@please.net> - 2018-09-16 20:18 +1000
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-16 12:25 +0100
Re: arm-gcc: pointer to constant string Clifford Heath <no.spam@please.net> - 2018-09-16 22:22 +1000
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-16 15:00 +0200
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-16 14:33 +0100
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-16 22:06 +0200
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-16 21:42 +0100
Re: arm-gcc: pointer to constant string Les Cargill <lcargill99@comcast.com> - 2018-09-17 21:24 -0500
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-18 08:49 +0200
Re: arm-gcc: pointer to constant string Les Cargill <lcargill99@comcast.com> - 2018-09-21 22:15 -0500
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-22 11:53 +0200
Testing (Was: arm-gcc: pointer to constant string) Jacob Sparre Andersen <jacob@jacob-sparre.dk> - 2018-09-22 12:16 +0200
Re: Testing (Was: arm-gcc: pointer to constant string) David Brown <david.brown@hesbynett.no> - 2018-09-22 13:31 +0200
Re: Testing (Was: arm-gcc: pointer to constant string) Clifford Heath <no.spam@please.net> - 2018-09-23 09:26 +1000
Re: arm-gcc: pointer to constant string Niklas Holsti <niklas.holsti@tidorum.invalid> - 2018-09-22 20:06 +0300
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-23 14:39 +0200
Re: arm-gcc: pointer to constant string Les Cargill <lcargill99@comcast.com> - 2018-09-22 13:50 -0500
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-23 15:21 +0200
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-23 16:06 +0100
Re: arm-gcc: pointer to constant string julio@diegidio.name - 2018-09-23 08:41 -0700
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-23 16:49 +0100
Re: arm-gcc: pointer to constant string julio@diegidio.name - 2018-09-23 08:56 -0700
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-23 18:20 +0100
Re: arm-gcc: pointer to constant string julio@diegidio.name - 2018-09-23 12:05 -0700
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-23 20:50 +0100
Re: arm-gcc: pointer to constant string Les Cargill <lcargill99@comcast.com> - 2018-09-23 12:04 -0500
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-23 18:27 +0100
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-23 19:37 +0200
Re: arm-gcc: pointer to constant string Jacob Sparre Andersen <jacob@jacob-sparre.dk> - 2018-09-24 12:53 +0200
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-24 13:49 +0200
Re: arm-gcc: pointer to constant string Les Cargill <lcargill99@comcast.com> - 2018-09-28 20:17 -0500
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-18 08:32 +0100
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-18 10:02 +0200
Re: arm-gcc: pointer to constant string Les Cargill <lcargill99@comcast.com> - 2018-09-21 22:17 -0500
Re: arm-gcc: pointer to constant string Stef <stef33d@yahooI-N-V-A-L-I-D.com.invalid> - 2018-09-14 18:30 +0200
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-14 20:46 +0200
Re: arm-gcc: pointer to constant string Stefan Reuther <stefan.news@arcor.de> - 2018-09-14 19:57 +0200
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-14 20:56 +0200
Re: arm-gcc: pointer to constant string Stefan Reuther <stefan.news@arcor.de> - 2018-09-15 18:32 +0200
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-16 15:06 +0200
Re: arm-gcc: pointer to constant string Richard Damon <Richard@Damon-Family.org> - 2018-09-14 19:59 -0400
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-15 16:25 +0200
Re: arm-gcc: pointer to constant string Tauno Voipio <tauno.voipio@notused.fi.invalid> - 2018-09-14 13:49 +0300
Page 2 of 4 — ← Prev page 1 [2] 3 4 Next page →
| From | Clifford Heath <no.spam@please.net> |
|---|---|
| Date | 2018-09-16 22:22 +1000 |
| Message-ID | <YVrnD.102764$RN2.92597@fx40.iad> |
| In reply to | #28031 |
On 16/09/18 21:25, Tom Gardner wrote: > On 16/09/18 11:18, Clifford Heath wrote: >> On 16/09/18 17:42, Tom Gardner wrote: >>> On 16/09/18 04:58, Clifford Heath wrote: >>>> On 16/09/18 02:28, Tom Gardner wrote: >>>>> I know of three languages where subsetting is a practical >>>>> necessity: C, C++, and the SPARK subset of Ada. That's >>>>> significant. >>>>> >>>>> However SPARK's objective and *ability* is something that >>>>> C/C++ cannot even dream of: provably correct implementation >>>>> for use in high integrity systems. To get that you would have >>>>> to subset /any/ language (except possible NewSpeak!). >>>> >>>> You must be unfamiliar with the *formally proven* C compiler >>>> that was part of the sel4 (formally-proven microkernel) project. >>>> I've met some of the people, who work here in Sydney. >>>> >>>> They proved the operating system guarantees *down to the silicon* >>>> for a specific ARM 9 chip (with MMU). >>> >>> Reference please, and has the claim withstood knowledgeable >>> scrutiny? >>> >>> How did they formally prove the compiler? That in itself is >>> "entertaining" for an incompletely defined language such as C. >>> >>> Does "down to the silicon" include the silicon itself? >>> >>> The A9s are complex devices with caches, interrupts etc. >>> How was the effect of those taken into account in the proof? >> >> It it too hard for you to type "sel4" into Google? > > Google orders results on what it thinks you are interested > in :( It is easy for you to provide a definitive link. > > >> The first hit is <https://sel4.systems>, but there are >> many resources for this, including the backgrounder >> on L4 family microkernels on Wikipedia. > > The sel4 FAQ includes "The reduced proof assumptions mean > that we do not need to trust the compiler or linker, but > there may still be faults remaining in specific low-level > parts of the kernel (TLB, cache handling, handwritten > assembly, boot code). These parts are thoroughly manually > reviewed." and "From C code to binary code, we employ a > set of automated widely-used verification tools. These > are: SONOLAR, Z3, Isabelle/HOL, and HOL4." > > That looks like the *compiler* isn't formally verified. The C code is annotated with special comments that contain guidance for the automated provers. The provers analyse the C code, and the final binary, and (using knowledge of both C and the ARM instruction set) can formally prove the equivalence. So no, the compiler is not proven - but all of its specific outputs are proven to be an accurate translation of the respective inputs. That's good enough. It might not work for all possible C code, but it doesn't need to; it just needs to work for the actual code being compiled. > It also makes me ask the question as to whether C is > "merely" an intermediate language autogenerated from a > HOL spec. No. However the specification (the invariants that must be proved) are written in literate Haskell. >> This is the culmination of a massive multi-decade effort >> by some of the world's smartest people. It's not some >> maverick's hobby. > > I've seen many such activities since the early 80s, some > of them also based on LCF. They went nowhere. There has been no result like this anywhere before, period. Besides that, sel4 and its precursors are already in significant deployments, but guess what? They're all secure systems and don't tend to talk about it. Clifford Heath.
[toc] | [prev] | [next] | [standalone]
| From | David Brown <david.brown@hesbynett.no> |
|---|---|
| Date | 2018-09-16 15:00 +0200 |
| Message-ID | <pnlk5e$ntf$1@dont-email.me> |
| In reply to | #28023 |
On 15/09/18 18:28, Tom Gardner wrote: > On 15/09/18 15:24, David Brown wrote: >> On 14/09/18 21:51, Tom Gardner wrote: >>> On 14/09/18 19:37, David Brown wrote: >>>> On 14/09/18 19:45, Tom Gardner wrote: >>>>> On 14/09/18 16:02, David Brown wrote: >> >> <snip> >> >>>>>> With C, there are three standards to choose from - C90, C99 and C11. >>>>>> (There is an upcoming C17, but it is basically a bug-fix and >>>>>> occasional >>>>>> improved wording, so there is not much to be found there except nicer >>>>>> typesetting.) >>>>>> >>>>>> And there are also implementation-specific extensions - both compiler >>>>>> specific and target-specific. >>>>> >>>>> Don't forget the commercially important /subsets/! The need >>>>> for subsets is a warning flag in itself. >>>>> >>>> >>>> What need of "commercially important subsets" are you talking about? >>> >>> MISRA-C, for example. >> >> That is a set of rules for C, rather than a subset as such. > > That's hairsplitting, which obscures rather than illuminates. It is no different than programming in Forth, Ada, Python, Fortran, or any other language. What makes you think C is special? > > >> (And 90% of it could be replaced by three rules - 1. Learn the >> language properly and don't write invalid code. 2. Write in a >> readable fashion. 3. Get proper tools and learn how to use them.) > > Nonsense. You haven't read the Misra rules, have you? I didn't mention that the remaining 10% of the rules go against the C standards and compiler norms by inventing their own non-standard type system. I suppose that /does/ mean it counts as another type of C, but it is certainly not a standard one. > > >> Of course if a specific task, project, employer or customer has rules >> for how you work, you need to know them and follow them. But that is >> not "a subset of the language", or the fault of the language. > > I know of three languages where subsetting is a practical > necessity: C, C++, and the SPARK subset of Ada. That's > significant. I think you'll find it applies to /all/ programming languages. For some languages, there is enough consensus in these "subsets" and enough popularity of them that they are known popularly - like SPARK and MISRA. For others, they will be smaller. If company guidelines say that when programming Python you must use capital letters for class names and never write "from module import *", then you have a subset of the language just as surely as if they say "use MISRA for C". > > However SPARK's objective and *ability* is something that > C/C++ cannot even dream of: provably correct implementation > for use in high integrity systems. To get that you would have > to subset /any/ language (except possible NewSpeak!). > I know that is SPARK's objective. Most sets of guidelines or coding standards aim towards more reliable and less error-prone coding (though few aspire to claiming they can be provably correct). > > >>>> There /are/ compilers that implement subsets of C standards. But I >>>> don't see a /need/ for them. >>>> >>>>> >>>>> >>>>>> Generally, it is not hard to know which C version you are dealing >>>>>> with, >>>>>> and there is very little code that is valid in one version that is >>>>>> not >>>>>> equally valid in later versions. >>>>> >>>>> That statement, while correct, skims over a significant problem: >>>>> unfortunately too few people understand and can /predict/ what is >>>>> valid and invalid. >>>> >>>> Of course they can. Very few people ever write code that is valid >>>> C90 code and not valid C99 or C11 code. There are /very/ few >>>> incompatibilities. About the only one of significance I can think of >>>> is that functions no longer have implicit declarations. What >>>> examples can you give of reasonable, valid C90 code that is not C99 >>>> compatible, or C99 code that is not C11 compatible? Or C99 code that >>>> is not gnu99 compatible? >>> >>> You miss my point. >> >> Not unlikely! >> >>> >>> I am not arguing about the /differences/ between, say C99 and C11, >>> but C of /any/ standard. >> >> I still don't get it. Do you mean, say, the difference between C99 on >> gcc and C99 on IAR ? Or the difference between C on an ARM and C on >> an AVR? > > No. Very, /very/ few - if any - developers understand > all the undefined and implementation defined behaviour > of any standard of C or C++, and how to reconcile different > parts of the same standard (or differing implementations > of the same standard)! I think I see what you are getting at now - you are saying there are things in C that are undefined (or implementation-defined) that many C programmers don't realise are a problem. Yes, I can agree with that - though I think the problem is often overrated. The great majority of undefined behaviour in C is obviously undefined because there is no sensible definition for it - and there is no way anyone could reasonably expect code to "work". That applies to things like buffer overruns, out of bounds pointers, etc. The most obvious category of undefined behaviours where people get things wrong are, I would say, accessing data through incompatible pointers and signed integer overflow. In the case of signed integer overflow, the code is almost certainly wrong regardless of any definition of the behaviour. The rest is just a matter of not knowing the language as well as they should, and thus getting things wrong. That happens in all languages. I am not in any way saying that C or C++ are perfect languages, or that their standards are ideal, or anything like that. I am merely saying they are not as bad as many people make out, and not different in principle from other languages. > > Statements from those that were involved in some of the > standardisation efforts lead me to believe that's also > the case for > - commercial compiler writers, several of whom have had > requested requested opinions about how standard clause > X can be reconciled with standard clause Y > - the committee itself, e.g. infamously with their refusal to > believe C++ templates were Turing complete until somebody > rubbed their faces in proof! > > No, I can't quote chapter and verse. While watching the > shenanigans from the sidelines it became apparent to me > that C/C++ was becoming (early/mid 90s) part of the problem > as well as part of the solution.
[toc] | [prev] | [next] | [standalone]
| From | Tom Gardner <spamjunk@blueyonder.co.uk> |
|---|---|
| Date | 2018-09-16 14:33 +0100 |
| Message-ID | <7ZsnD.408545$%L2.113927@fx15.am4> |
| In reply to | #28034 |
On 16/09/18 14:00, David Brown wrote: > On 15/09/18 18:28, Tom Gardner wrote: >> On 15/09/18 15:24, David Brown wrote: >>> On 14/09/18 21:51, Tom Gardner wrote: >>>> On 14/09/18 19:37, David Brown wrote: >>>>> On 14/09/18 19:45, Tom Gardner wrote: >>>>>> On 14/09/18 16:02, David Brown wrote: >>> >>> <snip> >>> >>>>>>> With C, there are three standards to choose from - C90, C99 and C11. >>>>>>> (There is an upcoming C17, but it is basically a bug-fix and occasional >>>>>>> improved wording, so there is not much to be found there except nicer >>>>>>> typesetting.) >>>>>>> >>>>>>> And there are also implementation-specific extensions - both compiler >>>>>>> specific and target-specific. >>>>>> >>>>>> Don't forget the commercially important /subsets/! The need >>>>>> for subsets is a warning flag in itself. >>>>>> >>>>> >>>>> What need of "commercially important subsets" are you talking about? >>>> >>>> MISRA-C, for example. >>> >>> That is a set of rules for C, rather than a subset as such. >> >> That's hairsplitting, which obscures rather than illuminates. > > It is no different than programming in Forth, Ada, Python, Fortran, or any other > language. What makes you think C is special? > >> >> >>> (And 90% of it could be replaced by three rules - 1. Learn the language >>> properly and don't write invalid code. 2. Write in a readable fashion. 3. >>> Get proper tools and learn how to use them.) >> >> Nonsense. > > You haven't read the Misra rules, have you? I didn't mention that the remaining > 10% of the rules go against the C standards and compiler norms by inventing > their own non-standard type system. I suppose that /does/ mean it counts as > another type of C, but it is certainly not a standard one. If the type system is a valid use of C, then it is no more non-standard than libraries that aren't defined in the standard. >>> Of course if a specific task, project, employer or customer has rules for how >>> you work, you need to know them and follow them. But that is not "a subset >>> of the language", or the fault of the language. >> >> I know of three languages where subsetting is a practical >> necessity: C, C++, and the SPARK subset of Ada. That's >> significant. > > I think you'll find it applies to /all/ programming languages. For some > languages, there is enough consensus in these "subsets" and enough popularity of > them that they are known popularly - like SPARK and MISRA. For others, they > will be smaller. If company guidelines say that when programming Python you > must use capital letters for class names and never write "from module import *", > then you have a subset of the language just as surely as if they say "use MISRA > for C". I think most people would look askance at that being an informative definition of "subset" - and would instantly think to look at what's being concealed. >> However SPARK's objective and *ability* is something that >> C/C++ cannot even dream of: provably correct implementation >> for use in high integrity systems. To get that you would have >> to subset /any/ language (except possible NewSpeak!). >> > > I know that is SPARK's objective. Most sets of guidelines or coding standards > aim towards more reliable and less error-prone coding (though few aspire to > claiming they can be provably correct). Agreed. Overall I'm not a fan of formal proofs except in a few very niche applications. The proofs always have hard (in multiple senses) boundaries which exclude important real-world problems. >>>>> There /are/ compilers that implement subsets of C standards. But I don't >>>>> see a /need/ for them. >>>>> >>>>>> >>>>>> >>>>>>> Generally, it is not hard to know which C version you are dealing with, >>>>>>> and there is very little code that is valid in one version that is not >>>>>>> equally valid in later versions. >>>>>> >>>>>> That statement, while correct, skims over a significant problem: >>>>>> unfortunately too few people understand and can /predict/ what is >>>>>> valid and invalid. >>>>> >>>>> Of course they can. Very few people ever write code that is valid C90 code >>>>> and not valid C99 or C11 code. There are /very/ few incompatibilities. >>>>> About the only one of significance I can think of is that functions no >>>>> longer have implicit declarations. What examples can you give of >>>>> reasonable, valid C90 code that is not C99 compatible, or C99 code that is >>>>> not C11 compatible? Or C99 code that is not gnu99 compatible? >>>> >>>> You miss my point. >>> >>> Not unlikely! >>> >>>> >>>> I am not arguing about the /differences/ between, say C99 and C11, >>>> but C of /any/ standard. >>> >>> I still don't get it. Do you mean, say, the difference between C99 on gcc >>> and C99 on IAR ? Or the difference between C on an ARM and C on an AVR? >> >> No. Very, /very/ few - if any - developers understand >> all the undefined and implementation defined behaviour >> of any standard of C or C++, and how to reconcile different >> parts of the same standard (or differing implementations >> of the same standard)! > > I think I see what you are getting at now - you are saying there are things in C > that are undefined (or implementation-defined) that many C programmers don't > realise are a problem. Yes, I can agree with that - though I think the problem > is often overrated. The great majority of undefined behaviour in C is obviously > undefined because there is no sensible definition for it - and there is no way > anyone could reasonably expect code to "work". That applies to things like > buffer overruns, out of bounds pointers, etc. The most obvious category of > undefined behaviours where people get things wrong are, I would say, accessing > data through incompatible pointers and signed integer overflow. In the case of > signed integer overflow, the code is almost certainly wrong regardless of any > definition of the behaviour. > > The rest is just a matter of not knowing the language as well as they should, > and thus getting things wrong. That happens in all languages. > > I am not in any way saying that C or C++ are perfect languages, or that their > standards are ideal, or anything like that. I am merely saying they are not as > bad as many people make out, and not different in principle from other languages. There are no perfect languages, and probably cannot be. However, some languages are significantly more/less imperfect in practical use than others. Overall C has expanded until its rough edges have become part of the problem rather than part of the solution. Once it really was the best language for many purposes - but we have learned Better Techniques in the past 40 years. Cs position is firm for the same reason than COBOL's position is firm: history, familiarity and weight of existing code.
[toc] | [prev] | [next] | [standalone]
| From | David Brown <david.brown@hesbynett.no> |
|---|---|
| Date | 2018-09-16 22:06 +0200 |
| Message-ID | <pnmd4r$3h8$1@dont-email.me> |
| In reply to | #28036 |
On 16/09/18 15:33, Tom Gardner wrote: > On 16/09/18 14:00, David Brown wrote: >> On 15/09/18 18:28, Tom Gardner wrote: >>> On 15/09/18 15:24, David Brown wrote: >>>> On 14/09/18 21:51, Tom Gardner wrote: >>>>> On 14/09/18 19:37, David Brown wrote: >>>>>> On 14/09/18 19:45, Tom Gardner wrote: >>>>>>> On 14/09/18 16:02, David Brown wrote: >>>> >>>> <snip> >>>> >>>>>>>> With C, there are three standards to choose from - C90, C99 and >>>>>>>> C11. >>>>>>>> (There is an upcoming C17, but it is basically a bug-fix and >>>>>>>> occasional >>>>>>>> improved wording, so there is not much to be found there except >>>>>>>> nicer >>>>>>>> typesetting.) >>>>>>>> >>>>>>>> And there are also implementation-specific extensions - both >>>>>>>> compiler >>>>>>>> specific and target-specific. >>>>>>> >>>>>>> Don't forget the commercially important /subsets/! The need >>>>>>> for subsets is a warning flag in itself. >>>>>>> >>>>>> >>>>>> What need of "commercially important subsets" are you talking about? >>>>> >>>>> MISRA-C, for example. >>>> >>>> That is a set of rules for C, rather than a subset as such. >>> >>> That's hairsplitting, which obscures rather than illuminates. >> >> It is no different than programming in Forth, Ada, Python, Fortran, or >> any other language. What makes you think C is special? >> >>> >>> >>>> (And 90% of it could be replaced by three rules - 1. Learn the >>>> language properly and don't write invalid code. 2. Write in a >>>> readable fashion. 3. Get proper tools and learn how to use them.) >>> >>> Nonsense. >> >> You haven't read the Misra rules, have you? I didn't mention that the >> remaining 10% of the rules go against the C standards and compiler >> norms by inventing their own non-standard type system. I suppose that >> /does/ mean it counts as another type of C, but it is certainly not a >> standard one. > > If the type system is a valid use of C, then it is no more > non-standard than libraries that aren't defined in the standard. > Unfortunately, MISRA's idea of "essential types" is not /quite/ compatible with actual C. I have forgotten the details (and they may vary between MISRA versions), but there are points in which the MISRA rules say code should do something that is different from what the C rules say. I have seen at least one case where a (massively expensive) compiler generated code regarding integer promotions that was "MISRA correct" but not "C standards correct". > > >>>> Of course if a specific task, project, employer or customer has >>>> rules for how you work, you need to know them and follow them. But >>>> that is not "a subset of the language", or the fault of the language. >>> >>> I know of three languages where subsetting is a practical >>> necessity: C, C++, and the SPARK subset of Ada. That's >>> significant. >> >> I think you'll find it applies to /all/ programming languages. For >> some languages, there is enough consensus in these "subsets" and >> enough popularity of them that they are known popularly - like SPARK >> and MISRA. For others, they will be smaller. If company guidelines >> say that when programming Python you must use capital letters for >> class names and never write "from module import *", then you have a >> subset of the language just as surely as if they say "use MISRA for C". > > I think most people would look askance at that being an informative > definition of "subset" - and would instantly think to look at what's > being concealed. > > >>> However SPARK's objective and *ability* is something that >>> C/C++ cannot even dream of: provably correct implementation >>> for use in high integrity systems. To get that you would have >>> to subset /any/ language (except possible NewSpeak!). >>> >> >> I know that is SPARK's objective. Most sets of guidelines or coding >> standards aim towards more reliable and less error-prone coding >> (though few aspire to claiming they can be provably correct). > > Agreed. > > Overall I'm not a fan of formal proofs except in a few very > niche applications. The proofs always have hard (in multiple > senses) boundaries which exclude important real-world problems. There are few cases where formal proofs are worth the time and costs involved. But I like - when possible - to write my code with a view that a formal proof /could/ be made if someone were to go to the effort. It is rare that you could prove a whole program - but not uncommon that you could (if you wanted to) prove many of the functions involved. Thinking in terms of pre-conditions, invariants, post-conditions, variants, specifications - that is all good stuff for writing solid code, even if you don't do so formally. > > >>>>>> There /are/ compilers that implement subsets of C standards. But >>>>>> I don't see a /need/ for them. >>>>>> >>>>>>> >>>>>>> >>>>>>>> Generally, it is not hard to know which C version you are >>>>>>>> dealing with, >>>>>>>> and there is very little code that is valid in one version that >>>>>>>> is not >>>>>>>> equally valid in later versions. >>>>>>> >>>>>>> That statement, while correct, skims over a significant problem: >>>>>>> unfortunately too few people understand and can /predict/ what is >>>>>>> valid and invalid. >>>>>> >>>>>> Of course they can. Very few people ever write code that is valid >>>>>> C90 code and not valid C99 or C11 code. There are /very/ few >>>>>> incompatibilities. About the only one of significance I can think >>>>>> of is that functions no longer have implicit declarations. What >>>>>> examples can you give of reasonable, valid C90 code that is not >>>>>> C99 compatible, or C99 code that is not C11 compatible? Or C99 >>>>>> code that is not gnu99 compatible? >>>>> >>>>> You miss my point. >>>> >>>> Not unlikely! >>>> >>>>> >>>>> I am not arguing about the /differences/ between, say C99 and C11, >>>>> but C of /any/ standard. >>>> >>>> I still don't get it. Do you mean, say, the difference between C99 >>>> on gcc and C99 on IAR ? Or the difference between C on an ARM and C >>>> on an AVR? >>> >>> No. Very, /very/ few - if any - developers understand >>> all the undefined and implementation defined behaviour >>> of any standard of C or C++, and how to reconcile different >>> parts of the same standard (or differing implementations >>> of the same standard)! >> >> I think I see what you are getting at now - you are saying there are >> things in C that are undefined (or implementation-defined) that many C >> programmers don't realise are a problem. Yes, I can agree with that - >> though I think the problem is often overrated. The great majority of >> undefined behaviour in C is obviously undefined because there is no >> sensible definition for it - and there is no way anyone could >> reasonably expect code to "work". That applies to things like buffer >> overruns, out of bounds pointers, etc. The most obvious category of >> undefined behaviours where people get things wrong are, I would say, >> accessing data through incompatible pointers and signed integer >> overflow. In the case of signed integer overflow, the code is almost >> certainly wrong regardless of any definition of the behaviour. >> >> The rest is just a matter of not knowing the language as well as they >> should, and thus getting things wrong. That happens in all languages. >> >> I am not in any way saying that C or C++ are perfect languages, or >> that their standards are ideal, or anything like that. I am merely >> saying they are not as bad as many people make out, and not different >> in principle from other languages. > > There are no perfect languages, and probably cannot be. > > However, some languages are significantly more/less > imperfect in practical use than others. > > Overall C has expanded until its rough edges have become > part of the problem rather than part of the solution. Once > it really was the best language for many purposes - but we > have learned Better Techniques in the past 40 years. Certainly I do not think C is the best choice of language for many of the types of use it is put to. I think most people who program in C would be more productive and write more correct code in other languages - and most programs that are written in C would be better written in other languages. > > Cs position is firm for the same reason than COBOL's position > is firm: history, familiarity and weight of existing code. Those are undoubtedly reasons for choosing C in many cases. But C is still the best choice for many purposes - and sometimes the only "choice".
[toc] | [prev] | [next] | [standalone]
| From | Tom Gardner <spamjunk@blueyonder.co.uk> |
|---|---|
| Date | 2018-09-16 21:42 +0100 |
| Message-ID | <%eznD.530584$bu.79765@fx17.am4> |
| In reply to | #28037 |
On 16/09/18 21:06, David Brown wrote: > On 16/09/18 15:33, Tom Gardner wrote: >> On 16/09/18 14:00, David Brown wrote: >>> On 15/09/18 18:28, Tom Gardner wrote: >>>> On 15/09/18 15:24, David Brown wrote: >>>>> On 14/09/18 21:51, Tom Gardner wrote: >>>>>> On 14/09/18 19:37, David Brown wrote: >>>>>>> On 14/09/18 19:45, Tom Gardner wrote: >>>>>>>> On 14/09/18 16:02, David Brown wrote: >>>>> >>>>> <snip> >>>>> >>>>>>>>> With C, there are three standards to choose from - C90, C99 and C11. >>>>>>>>> (There is an upcoming C17, but it is basically a bug-fix and occasional >>>>>>>>> improved wording, so there is not much to be found there except nicer >>>>>>>>> typesetting.) >>>>>>>>> >>>>>>>>> And there are also implementation-specific extensions - both compiler >>>>>>>>> specific and target-specific. >>>>>>>> >>>>>>>> Don't forget the commercially important /subsets/! The need >>>>>>>> for subsets is a warning flag in itself. >>>>>>>> >>>>>>> >>>>>>> What need of "commercially important subsets" are you talking about? >>>>>> >>>>>> MISRA-C, for example. >>>>> >>>>> That is a set of rules for C, rather than a subset as such. >>>> >>>> That's hairsplitting, which obscures rather than illuminates. >>> >>> It is no different than programming in Forth, Ada, Python, Fortran, or any >>> other language. What makes you think C is special? >>> >>>> >>>> >>>>> (And 90% of it could be replaced by three rules - 1. Learn the language >>>>> properly and don't write invalid code. 2. Write in a readable fashion. 3. >>>>> Get proper tools and learn how to use them.) >>>> >>>> Nonsense. >>> >>> You haven't read the Misra rules, have you? I didn't mention that the >>> remaining 10% of the rules go against the C standards and compiler norms by >>> inventing their own non-standard type system. I suppose that /does/ mean it >>> counts as another type of C, but it is certainly not a standard one. >> >> If the type system is a valid use of C, then it is no more >> non-standard than libraries that aren't defined in the standard. >> > > Unfortunately, MISRA's idea of "essential types" is not /quite/ compatible with > actual C. I have forgotten the details (and they may vary between MISRA > versions), but there are points in which the MISRA rules say code should do > something that is different from what the C rules say. I have seen at least one > case where a (massively expensive) compiler generated code regarding integer > promotions that was "MISRA correct" but not "C standards correct". > >> >> >>>>> Of course if a specific task, project, employer or customer has rules for >>>>> how you work, you need to know them and follow them. But that is not "a >>>>> subset of the language", or the fault of the language. >>>> >>>> I know of three languages where subsetting is a practical >>>> necessity: C, C++, and the SPARK subset of Ada. That's >>>> significant. >>> >>> I think you'll find it applies to /all/ programming languages. For some >>> languages, there is enough consensus in these "subsets" and enough popularity >>> of them that they are known popularly - like SPARK and MISRA. For others, >>> they will be smaller. If company guidelines say that when programming Python >>> you must use capital letters for class names and never write "from module >>> import *", then you have a subset of the language just as surely as if they >>> say "use MISRA for C". >> >> I think most people would look askance at that being an informative definition >> of "subset" - and would instantly think to look at what's being concealed. >> >> >>>> However SPARK's objective and *ability* is something that >>>> C/C++ cannot even dream of: provably correct implementation >>>> for use in high integrity systems. To get that you would have >>>> to subset /any/ language (except possible NewSpeak!). >>>> >>> >>> I know that is SPARK's objective. Most sets of guidelines or coding >>> standards aim towards more reliable and less error-prone coding (though few >>> aspire to claiming they can be provably correct). >> >> Agreed. >> >> Overall I'm not a fan of formal proofs except in a few very >> niche applications. The proofs always have hard (in multiple >> senses) boundaries which exclude important real-world problems. > > There are few cases where formal proofs are worth the time and costs involved. > But I like - when possible - to write my code with a view that a formal proof > /could/ be made if someone were to go to the effort. It is rare that you could > prove a whole program - but not uncommon that you could (if you wanted to) prove > many of the functions involved. Thinking in terms of pre-conditions, invariants, > post-conditions, variants, specifications - that is all good stuff for writing > solid code, even if you don't do so formally. > >> >> >>>>>>> There /are/ compilers that implement subsets of C standards. But I don't >>>>>>> see a /need/ for them. >>>>>>> >>>>>>>> >>>>>>>> >>>>>>>>> Generally, it is not hard to know which C version you are dealing with, >>>>>>>>> and there is very little code that is valid in one version that is not >>>>>>>>> equally valid in later versions. >>>>>>>> >>>>>>>> That statement, while correct, skims over a significant problem: >>>>>>>> unfortunately too few people understand and can /predict/ what is >>>>>>>> valid and invalid. >>>>>>> >>>>>>> Of course they can. Very few people ever write code that is valid C90 >>>>>>> code and not valid C99 or C11 code. There are /very/ few >>>>>>> incompatibilities. About the only one of significance I can think of is >>>>>>> that functions no longer have implicit declarations. What examples can >>>>>>> you give of reasonable, valid C90 code that is not C99 compatible, or C99 >>>>>>> code that is not C11 compatible? Or C99 code that is not gnu99 compatible? >>>>>> >>>>>> You miss my point. >>>>> >>>>> Not unlikely! >>>>> >>>>>> >>>>>> I am not arguing about the /differences/ between, say C99 and C11, >>>>>> but C of /any/ standard. >>>>> >>>>> I still don't get it. Do you mean, say, the difference between C99 on gcc >>>>> and C99 on IAR ? Or the difference between C on an ARM and C on an AVR? >>>> >>>> No. Very, /very/ few - if any - developers understand >>>> all the undefined and implementation defined behaviour >>>> of any standard of C or C++, and how to reconcile different >>>> parts of the same standard (or differing implementations >>>> of the same standard)! >>> >>> I think I see what you are getting at now - you are saying there are things >>> in C that are undefined (or implementation-defined) that many C programmers >>> don't realise are a problem. Yes, I can agree with that - though I think the >>> problem is often overrated. The great majority of undefined behaviour in C >>> is obviously undefined because there is no sensible definition for it - and >>> there is no way anyone could reasonably expect code to "work". That applies >>> to things like buffer overruns, out of bounds pointers, etc. The most >>> obvious category of undefined behaviours where people get things wrong are, I >>> would say, accessing data through incompatible pointers and signed integer >>> overflow. In the case of signed integer overflow, the code is almost >>> certainly wrong regardless of any definition of the behaviour. >>> >>> The rest is just a matter of not knowing the language as well as they should, >>> and thus getting things wrong. That happens in all languages. >>> >>> I am not in any way saying that C or C++ are perfect languages, or that their >>> standards are ideal, or anything like that. I am merely saying they are not >>> as bad as many people make out, and not different in principle from other >>> languages. >> >> There are no perfect languages, and probably cannot be. >> >> However, some languages are significantly more/less >> imperfect in practical use than others. >> >> Overall C has expanded until its rough edges have become >> part of the problem rather than part of the solution. Once >> it really was the best language for many purposes - but we >> have learned Better Techniques in the past 40 years. > > Certainly I do not think C is the best choice of language for many of the types > of use it is put to. I think most people who program in C would be more > productive and write more correct code in other languages - and most programs > that are written in C would be better written in other languages. > >> >> Cs position is firm for the same reason than COBOL's position >> is firm: history, familiarity and weight of existing code. > > Those are undoubtedly reasons for choosing C in many cases. But C is still the > best choice for many purposes - and sometimes the only "choice". Oh dear. I can't find /anything/ to disagree with in those statements :)
[toc] | [prev] | [next] | [standalone]
| From | Les Cargill <lcargill99@comcast.com> |
|---|---|
| Date | 2018-09-17 21:24 -0500 |
| Message-ID | <pnpn9t$i6j$1@dont-email.me> |
| In reply to | #28037 |
David Brown wrote: > On 16/09/18 15:33, Tom Gardner wrote: >> On 16/09/18 14:00, David Brown wrote: <snip> > > There are few cases where formal proofs are worth the time and costs > involved. But I like - when possible - to write my code with a view > that a formal proof /could/ be made if someone were to go to the effort. > It is rare that you could prove a whole program - but not uncommon > that you could (if you wanted to) prove many of the functions involved. > Thinking in terms of pre-conditions, invariants, post-conditions, > variants, specifications - that is all good stuff for writing solid > code, even if you don't do so formally. > If you stick to something akin to the Haskell Actor model and everything is an event, it's not too onerous to use combinators to generate a significant subset of all messages. With the proper level of introspection, you can "prove" the program works to a limit enumerated by the test vectors and that it continues to do so as changes are made to the code base. The test vectors and captured output can be controlled and compared to. And if you want to go as far as model checking or partial model checking, you have the stuff in place to enforce that now. Obviously, there are domains where you just can't get close enough to this ideal. So you gamble. <snip> > > Certainly I do not think C is the best choice of language for many of > the types of use it is put to. I think most people who program in C > would be more productive and write more correct code in other languages > - and most programs that are written in C would be better written in > other languages. > Possibly. But what C offers is the ability to build nonstandard, hybrid "furniture" to support the development effort that can not be forseen by language and library designers. This is especially pronounced in serialization and the ability to dynamically configure a program ( which are two sides of the same coin ). C also supports event-driven-ness in a way that few other languages do. <snip> -- Les Cargill
[toc] | [prev] | [next] | [standalone]
| From | David Brown <david.brown@hesbynett.no> |
|---|---|
| Date | 2018-09-18 08:49 +0200 |
| Message-ID | <pnq76n$kos$1@dont-email.me> |
| In reply to | #28043 |
On 18/09/18 04:24, Les Cargill wrote: > David Brown wrote: >> On 16/09/18 15:33, Tom Gardner wrote: >>> On 16/09/18 14:00, David Brown wrote: > <snip> >> >> There are few cases where formal proofs are worth the time and costs >> involved. But I like - when possible - to write my code with a view >> that a formal proof /could/ be made if someone were to go to the >> effort. It is rare that you could prove a whole program - but not >> uncommon that you could (if you wanted to) prove many of the functions >> involved. Thinking in terms of pre-conditions, invariants, >> post-conditions, variants, specifications - that is all good stuff for >> writing solid code, even if you don't do so formally. >> > > If you stick to something akin to the Haskell Actor model and everything > is an event, it's not too onerous to use combinators to generate a > significant subset of all messages. With the proper level of > introspection, you can "prove" the program works to a limit > enumerated by the test vectors and that it continues to do so as > changes are made to the code base. > Testing can /never/ prove a program is correct - unless you can enumerate /all/ inputs and states of your code and go through them all. Testing can prove a program is wrong (and it is vital for that), but it cannot prove a program is correct. A functional programming language like Haskell gives you a much better chance of actually proving the correctness of your code than an imperative language like C - that is one of the reasons for the existence of functional programming languages (it is the lack of state and side-effects that help). But if you want to prove the correctness of your Haskell program, you do it by an analysis of the code, or by deriving correct code in the first place - you don't do it by testing. > The test vectors and captured output can be controlled and > compared to. And if you want to go as far as model > checking or partial model checking, you have the stuff in place to > enforce that now. > > > Obviously, there are domains where you just can't get close enough to > this ideal. So you gamble. > Indeed - and almost all practical situations fall into this category. > <snip> > >> >> Certainly I do not think C is the best choice of language for many of >> the types of use it is put to. I think most people who program in C >> would be more productive and write more correct code in other >> languages - and most programs that are written in C would be better >> written in other languages. >> > > Possibly. But what C offers is the ability to build nonstandard, hybrid > "furniture" to support the development effort that can not be > forseen by language and library designers. This is especially pronounced > in serialization and the ability to dynamically configure a program ( > which are two sides of the same coin ). > I don't follow that at all. > C also supports event-driven-ness in a way that few other languages do. > And I follow that even less. (I am not saying I disagree with you, I just can't see what you are trying to say. Maybe I'll understand it better after some coffee.) C certainly has its important features and strengths, and is a very useful language to have.
[toc] | [prev] | [next] | [standalone]
| From | Les Cargill <lcargill99@comcast.com> |
|---|---|
| Date | 2018-09-21 22:15 -0500 |
| Message-ID | <po4bpk$5nm$1@dont-email.me> |
| In reply to | #28044 |
David Brown wrote: > On 18/09/18 04:24, Les Cargill wrote: >> David Brown wrote: >>> On 16/09/18 15:33, Tom Gardner wrote: >>>> On 16/09/18 14:00, David Brown wrote: >> <snip> >>> >>> There are few cases where formal proofs are worth the time and costs >>> involved. But I like - when possible - to write my code with a view >>> that a formal proof /could/ be made if someone were to go to the >>> effort. It is rare that you could prove a whole program - but not >>> uncommon that you could (if you wanted to) prove many of the functions >>> involved. Thinking in terms of pre-conditions, invariants, >>> post-conditions, variants, specifications - that is all good stuff for >>> writing solid code, even if you don't do so formally. >>> >> >> If you stick to something akin to the Haskell Actor model and everything >> is an event, it's not too onerous to use combinators to generate a >> significant subset of all messages. With the proper level of >> introspection, you can "prove" the program works to a limit >> enumerated by the test vectors and that it continues to do so as >> changes are made to the code base. >> > > Testing can /never/ prove a program is correct - unless you can > enumerate /all/ inputs and states of your code and go through them all. > Testing can prove a program is wrong (and it is vital for that), but it > cannot prove a program is correct. > So what you can to is find the meat of what is possible and do that. I must say - I am rather tired of this old warhorse; an appeal to Godel in the form of an economics question. All I would say is that you should test as well as you can. You should use a dragon to fight the dragon. And so if your system is adept at rejecting inputs it cannot expect, then what? It's all about the ability to enforce constraints. Sort your constraints by the ability to do damage. > A functional programming language like Haskell gives you a much better > chance of actually proving the correctness of your code than an > imperative language like C - that is one of the reasons for the > existence of functional programming languages (it is the lack of state > and side-effects that help). But if you want to prove the correctness > of your Haskell program, you do it by an analysis of the code, or by > deriving correct code in the first place - you don't do it by testing. > That's because we'd like to pretend that "analysis" is some process that's not automatable. Or, at least, not somehow aided by automation. I only invoked Haskell because it's the source of the actor pattern. >> The test vectors and captured output can be controlled and >> compared to. And if you want to go as far as model >> checking or partial model checking, you have the stuff in place to >> enforce that now. >> >> >> Obviously, there are domains where you just can't get close enough to >> this ideal. So you gamble. >> > > Indeed - and almost all practical situations fall into this category. > Yeah, I dunno. I think people give up too early. >> <snip> >> >>> >>> Certainly I do not think C is the best choice of language for many of >>> the types of use it is put to. I think most people who program in C >>> would be more productive and write more correct code in other >>> languages - and most programs that are written in C would be better >>> written in other languages. >>> >> >> Possibly. But what C offers is the ability to build nonstandard, hybrid >> "furniture" to support the development effort that can not be >> forseen by language and library designers. This is especially pronounced >> in serialization and the ability to dynamically configure a program ( >> which are two sides of the same coin ). >> > > I don't follow that at all. > So write a C++ thing to dump all the state in Any Random C++ object to a text file. You can get close. A C struct? Gimme thirty minutes and the source code. >> C also supports event-driven-ness in a way that few other languages do. >> > > And I follow that even less. > And that's fine. I accept the following premises: - Model checking is the current state of the art in correctness. - Models don't work without events. - Models work better when they're introspected. - Because C can "cheat" and use the physical representation of objects in memory, it has a small leg up in the game of introspection. C has select()/poll()/epoll() and Real(tm) callbacks. > (I am not saying I disagree with you, I just can't see what you are > trying to say. Maybe I'll understand it better after some coffee.) > For what it is worth, If I knew what I was trying to way, I'd say it :) > C certainly has its important features and strengths, and is a very > useful language to have. > So the tack I've taken is to cobble together things that make C do what I want it to ( with a scripting language adept at string processing ) rather than wait on someone else to provide things for me. -- Les Cargill
[toc] | [prev] | [next] | [standalone]
| From | David Brown <david.brown@hesbynett.no> |
|---|---|
| Date | 2018-09-22 11:53 +0200 |
| Message-ID | <po53eb$poj$1@dont-email.me> |
| In reply to | #28082 |
On 22/09/18 05:15, Les Cargill wrote: > David Brown wrote: >> On 18/09/18 04:24, Les Cargill wrote: >>> David Brown wrote: >>>> On 16/09/18 15:33, Tom Gardner wrote: >>>>> On 16/09/18 14:00, David Brown wrote: >>> <snip> >>>> >>>> There are few cases where formal proofs are worth the time and costs >>>> involved. But I like - when possible - to write my code with a view >>>> that a formal proof /could/ be made if someone were to go to the >>>> effort. It is rare that you could prove a whole program - but not >>>> uncommon that you could (if you wanted to) prove many of the functions >>>> involved. Thinking in terms of pre-conditions, invariants, >>>> post-conditions, variants, specifications - that is all good stuff for >>>> writing solid code, even if you don't do so formally. >>>> >>> >>> If you stick to something akin to the Haskell Actor model and everything >>> is an event, it's not too onerous to use combinators to generate a >>> significant subset of all messages. With the proper level of >>> introspection, you can "prove" the program works to a limit >>> enumerated by the test vectors and that it continues to do so as >>> changes are made to the code base. >>> >> >> Testing can /never/ prove a program is correct - unless you can >> enumerate /all/ inputs and states of your code and go through them all. >> Testing can prove a program is wrong (and it is vital for that), but it >> cannot prove a program is correct. >> > > So what you can to is find the meat of what is possible and do that. > > I must say - I am rather tired of this old warhorse; an appeal to Godel > in the form of an economics question. All I would say is > that you should test as well as you can. You should use a dragon to > fight the dragon. No one will argue against the benefits of testing as well as you reasonably can. Testing is often good enough to reach the level of confidence you want for code. But you are simply /wrong/ to think that non-exhaustive testing can somehow "prove" that code works. And there are some classes of problem for which testing is extremely unlikely to identify the problem. In particular, for anything involving race conditions or timing, you cannot /test/ your way to working code. You have to write the code correctly in the first place, because the chances of spotting the microsecond window of disaster in your lab testing is tiny. (I am not saying you need to formally prove the code - again, this is all about appropriate balances of time and effort - but testing does not help.) > > And so if your system is adept at rejecting inputs it cannot expect, > then what? > > It's all about the ability to enforce constraints. Sort your > constraints by the ability to do damage. > >> A functional programming language like Haskell gives you a much better >> chance of actually proving the correctness of your code than an >> imperative language like C - that is one of the reasons for the >> existence of functional programming languages (it is the lack of state >> and side-effects that help). But if you want to prove the correctness >> of your Haskell program, you do it by an analysis of the code, or by >> deriving correct code in the first place - you don't do it by testing. >> > > That's because we'd like to pretend that "analysis" is some > process that's not automatable. Or, at least, not somehow aided by > automation. Analysis is much easier when you have restrictions on what can happen. In a pure functional programming language, your function takes some input and works solely on that input, and the only effect of the code is to generate the output. That means you can analyse it in isolation. In general C code, your function might use or change global state - it all quickly becomes a lot more complicated. <snip> > For what it is worth, If I knew what I was trying to way, I'd say it :) > OK. If you figure it out, we can take it up again - otherwise I think any replies I'd make would add to the confusion (mine, yours, or everyone else's).
[toc] | [prev] | [next] | [standalone]
| From | Jacob Sparre Andersen <jacob@jacob-sparre.dk> |
|---|---|
| Date | 2018-09-22 12:16 +0200 |
| Subject | Testing (Was: arm-gcc: pointer to constant string) |
| Message-ID | <87efdlu9af.fsf_-_@jacob-sparre.dk> |
| In reply to | #28086 |
David Brown wrote: > But you are simply /wrong/ to think that non-exhaustive testing can > somehow "prove" that code works. I hope we all agree on this. > And there are some classes of problem for which testing is extremely > unlikely to identify the problem. In particular, for anything > involving race conditions or timing, you cannot /test/ your way to > working code. If you know the possible origin of race conditions, you can actually detect them using faked versions of selected functions in an API. It still doesn't prove anything, and I'm not sure how often it is cost effective, but it is worth being aware of the possibility. We've done it on one legacy project I've worked on. The system is database-heavy, and has a high risk of problems due to race-conditions on database modifications. We created a modified version of the database API implementation, where we easily can inject what will appear as competing modifications of the database from other processes. It doesn't find all the problems, but it easily reveals to worst blunders. I am pretty sure you can do similar things in other cases - like file system interactions - but I'm not sure how often it is worth the effort. Maybe such a modified test implementation should be distributed with all libraries, where there is a serious risk of race-conditions in using the API. On the other hand, if you know that much, when you create a library, you might as well try to write the API so it (to the extent possible) lets the user avoid race-conditions completely. Greetings, Jacob -- "I remember being impressed with Ada because you could write an infinite loop without a faked up condition. The idea being that in Ada the typical infinite loop would normally be terminated by detonation." -- Larry Wall
[toc] | [prev] | [next] | [standalone]
| From | David Brown <david.brown@hesbynett.no> |
|---|---|
| Date | 2018-09-22 13:31 +0200 |
| Subject | Re: Testing (Was: arm-gcc: pointer to constant string) |
| Message-ID | <po596g$jav$1@dont-email.me> |
| In reply to | #28087 |
On 22/09/18 12:16, Jacob Sparre Andersen wrote: > David Brown wrote: > >> But you are simply /wrong/ to think that non-exhaustive testing can >> somehow "prove" that code works. > > I hope we all agree on this. > >> And there are some classes of problem for which testing is extremely >> unlikely to identify the problem. In particular, for anything >> involving race conditions or timing, you cannot /test/ your way to >> working code. > > If you know the possible origin of race conditions, you can actually > detect them using faked versions of selected functions in an API. It > still doesn't prove anything, and I'm not sure how often it is cost > effective, but it is worth being aware of the possibility. > > We've done it on one legacy project I've worked on. The system is > database-heavy, and has a high risk of problems due to race-conditions > on database modifications. We created a modified version of the > database API implementation, where we easily can inject what will appear > as competing modifications of the database from other processes. It > doesn't find all the problems, but it easily reveals to worst blunders. > > I am pretty sure you can do similar things in other cases - like file > system interactions - but I'm not sure how often it is worth the effort. > Maybe such a modified test implementation should be distributed with all > libraries, where there is a serious risk of race-conditions in using the > API. On the other hand, if you know that much, when you create a > library, you might as well try to write the API so it (to the extent > possible) lets the user avoid race-conditions completely. > That's a interesting idea. I have done something a little similar when tracing timing problems. Basically, if your problem occurs when event A happens during processing B, then stick a big slow loop in the middle of B and the crash becomes far more likely. (Tests can't prove your code has no bugs - but they /can/ prove your code /does/ have bugs, and can be helpful in finding them.)
[toc] | [prev] | [next] | [standalone]
| From | Clifford Heath <no.spam@please.net> |
|---|---|
| Date | 2018-09-23 09:26 +1000 |
| Subject | Re: Testing (Was: arm-gcc: pointer to constant string) |
| Message-ID | <AcApD.50623$fE2.46988@fx30.iad> |
| In reply to | #28088 |
On 22/09/18 21:31, David Brown wrote: > On 22/09/18 12:16, Jacob Sparre Andersen wrote: >> David Brown wrote: >> >>> But you are simply /wrong/ to think that non-exhaustive testing can >>> somehow "prove" that code works. >> >> I hope we all agree on this. >> >>> And there are some classes of problem for which testing is extremely >>> unlikely to identify the problem. In particular, for anything >>> involving race conditions or timing, you cannot /test/ your way to >>> working code. >> >> If you know the possible origin of race conditions, you can actually >> detect them using faked versions of selected functions in an API. It >> still doesn't prove anything, and I'm not sure how often it is cost >> effective, but it is worth being aware of the possibility. >> >> We've done it on one legacy project I've worked on. The system is >> database-heavy, and has a high risk of problems due to race-conditions >> on database modifications. We created a modified version of the >> database API implementation, where we easily can inject what will appear >> as competing modifications of the database from other processes. It >> doesn't find all the problems, but it easily reveals to worst blunders. >> >> I am pretty sure you can do similar things in other cases - like file >> system interactions - but I'm not sure how often it is worth the effort. >> Maybe such a modified test implementation should be distributed with all >> libraries, where there is a serious risk of race-conditions in using the >> API. On the other hand, if you know that much, when you create a >> library, you might as well try to write the API so it (to the extent >> possible) lets the user avoid race-conditions completely. >> > > That's a interesting idea. I have done something a little similar when > tracing timing problems. Basically, if your problem occurs when event A > happens during processing B, then stick a big slow loop in the middle of > B and the crash becomes far more likely. (Tests can't prove your code > has no bugs - but they /can/ prove your code /does/ have bugs, and can > be helpful in finding them.) There was a threading library I read about which had a debug/trace version you could link with. It recorded all thread scheduling based on its synchronisation primitives. If you hit an error case, you could replay the same test case and it would replay the exact same scheduling decisions for you, so you could debug the cause of the error. Presumably when a thread asked for a resource that was available (but which wasn't on the faulty run) it would block the thread until the correct sequence was able to be continued. I never used it, but that seems like a really good idea. Clifford Heath.
[toc] | [prev] | [next] | [standalone]
| From | Niklas Holsti <niklas.holsti@tidorum.invalid> |
|---|---|
| Date | 2018-09-22 20:06 +0300 |
| Message-ID | <g0nb4lFphqbU1@mid.individual.net> |
| In reply to | #28086 |
On 18-09-22 12:53 , David Brown wrote:
> On 22/09/18 05:15, Les Cargill wrote:
[on testing vs proof and analysis]
> No one will argue against the benefits of testing as well as you
> reasonably can. Testing is often good enough to reach the level of
> confidence you want for code.
>
> But you are simply /wrong/ to think that non-exhaustive testing can
> somehow "prove" that code works.
>
> And there are some classes of problem for which testing is extremely
> unlikely to identify the problem. In particular, for anything involving
> race conditions or timing, you cannot /test/ your way to working code.
> You have to write the code correctly in the first place, because the
> chances of spotting the microsecond window of disaster in your lab
> testing is tiny.
As you probably know, several static-analysis tools have the ability to
detect possible race conditions, as accesses to unprotected shared
variables from two or more threads/tasks.
I have used the AdaControl tool for this (and other) analysis of Ada
code, and found real race conditions.
The tool-based race-condition analyses are most likely imperfect (for
example, because shared variables are accessed via pointers), but
nevertheless useful.
--
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
. @ .
[toc] | [prev] | [next] | [standalone]
| From | David Brown <david.brown@hesbynett.no> |
|---|---|
| Date | 2018-09-23 14:39 +0200 |
| Message-ID | <po81j0$ugq$1@dont-email.me> |
| In reply to | #28098 |
On 22/09/18 19:06, Niklas Holsti wrote: > On 18-09-22 12:53 , David Brown wrote: >> On 22/09/18 05:15, Les Cargill wrote: > > [on testing vs proof and analysis] > >> No one will argue against the benefits of testing as well as you >> reasonably can. Testing is often good enough to reach the level of >> confidence you want for code. >> >> But you are simply /wrong/ to think that non-exhaustive testing can >> somehow "prove" that code works. >> >> And there are some classes of problem for which testing is extremely >> unlikely to identify the problem. In particular, for anything involving >> race conditions or timing, you cannot /test/ your way to working code. >> You have to write the code correctly in the first place, because the >> chances of spotting the microsecond window of disaster in your lab >> testing is tiny. > > As you probably know, several static-analysis tools have the ability to > detect possible race conditions, as accesses to unprotected shared > variables from two or more threads/tasks. > > I have used the AdaControl tool for this (and other) analysis of Ada > code, and found real race conditions. > > The tool-based race-condition analyses are most likely imperfect (for > example, because shared variables are accessed via pointers), but > nevertheless useful. > If you can detect problems via static analysis tools, that is always good - finding them early means you can fix them early. Another way to avoid some kinds of problems is through smart use of programming languages. C++ "tag" classes are useful here - you can use them to make some kinds of multitasking errors into type errors. For example, suppose you have two locks - A and B - and want to be sure that you can't take lock "B" unless you also have lock "A". Calls to function "foo" should only be done when you have lock "A", and calls to function "bar" should only be when you have lock "B". You can make an class "GotLockA" whose constructor acquires lock A and whose destructor releases it. This class can actually be empty - it does not have any values. (It is /not/ a wrapper around lock objects - it is a type for a /particular/ lock.) Function foo then takes a parameter of type GotLockA (it doesn't do anything with the parameter) - and now any code that tries to call "foo" without holding lock A is a compile time error. Similarly, you make a class GotLockB whose constructor requires a GotLockA instance and acquires lock B. You can then only call "bar" if you've got lock B, which also implies you have lock A. There is work to be done deciding about copying and moving these classes. But the principle is that you match the dynamic, run-time state of locks to static scope and types.
[toc] | [prev] | [next] | [standalone]
| From | Les Cargill <lcargill99@comcast.com> |
|---|---|
| Date | 2018-09-22 13:50 -0500 |
| Message-ID | <po62if$d9t$1@dont-email.me> |
| In reply to | #28086 |
David Brown wrote: > On 22/09/18 05:15, Les Cargill wrote: >> David Brown wrote: >>> On 18/09/18 04:24, Les Cargill wrote: >>>> David Brown wrote: >>>>> On 16/09/18 15:33, Tom Gardner wrote: >>>>>> On 16/09/18 14:00, David Brown wrote: >>>> <snip> >>>>> >>>>> There are few cases where formal proofs are worth the time and costs >>>>> involved. But I like - when possible - to write my code with a view >>>>> that a formal proof /could/ be made if someone were to go to the >>>>> effort. It is rare that you could prove a whole program - but not >>>>> uncommon that you could (if you wanted to) prove many of the functions >>>>> involved. Thinking in terms of pre-conditions, invariants, >>>>> post-conditions, variants, specifications - that is all good stuff for >>>>> writing solid code, even if you don't do so formally. >>>>> >>>> >>>> If you stick to something akin to the Haskell Actor model and >>>> everything >>>> is an event, it's not too onerous to use combinators to generate a >>>> significant subset of all messages. With the proper level of >>>> introspection, you can "prove" the program works to a limit >>>> enumerated by the test vectors and that it continues to do so as >>>> changes are made to the code base. >>>> >>> >>> Testing can /never/ prove a program is correct - unless you can >>> enumerate /all/ inputs and states of your code and go through them all. >>> Testing can prove a program is wrong (and it is vital for that), >>> but it >>> cannot prove a program is correct. >>> >> >> So what you can to is find the meat of what is possible and do that. >> >> I must say - I am rather tired of this old warhorse; an appeal to >> Godel in the form of an economics question. All I would say is >> that you should test as well as you can. You should use a dragon to >> fight the dragon. > > No one will argue against the benefits of testing as well as you > reasonably can. Testing is often good enough to reach the level of > confidence you want for code. > > But you are simply /wrong/ to think that non-exhaustive testing can > somehow "prove" that code works. > "Proof" isn't that interesting outside of certain contexts. By "proof" I mean fully formal verification that it's 100% known to be correct. We want to find a break-even variation on that. We want the cost and the risk to be commensurate. Turns out, just measuring the risk is pretty hard. > And there are some classes of problem for which testing is extremely > unlikely to identify the problem. In particular, for anything involving > race conditions or timing, you cannot /test/ your way to working code. Not in harness, but you can prove out the approach being used as a demonstration and reasoning tool. And it depend on the problem - you might be able to generate test vectors that get darned close. You point is probably "yes, but how close?" :) And it's a good one. As an example, I had a "one producer/one consumer" buffer. I wasn't 100% sure if it needed semaphores - one producer, one consumer, right? I thought about it a bit , built a driver loop and was able to prove that I did indeed need semaphores. To be fair, I was leaning that way anyway. > You have to write the code correctly in the first place, because the > chances of spotting the microsecond window of disaster in your lab > testing is tiny. (I am not saying you need to formally prove the code - > again, this is all about appropriate balances of time and effort - but > testing does not help.) > Maybe it's bias from seeing stuff online, but I get the feeling that many people ( and I'm pretty sure you, David, are not one of them ) just sort of despair of the whole thing. > >> >> And so if your system is adept at rejecting inputs it cannot expect, >> then what? >> >> It's all about the ability to enforce constraints. Sort your >> constraints by the ability to do damage. >> >>> A functional programming language like Haskell gives you a much better >>> chance of actually proving the correctness of your code than an >>> imperative language like C - that is one of the reasons for the >>> existence of functional programming languages (it is the lack of state >>> and side-effects that help). But if you want to prove the correctness >>> of your Haskell program, you do it by an analysis of the code, or by >>> deriving correct code in the first place - you don't do it by testing. >>> >> >> That's because we'd like to pretend that "analysis" is some >> process that's not automatable. Or, at least, not somehow aided by >> automation. > > Analysis is much easier when you have restrictions on what can happen. You said it man. :) > In a pure functional programming language, your function takes some > input and works solely on that input, and the only effect of the code is > to generate the output. That means you can analyse it in isolation. In > general C code, your function might use or change global state - it all > quickly becomes a lot more complicated. > But the thing you must learn with C is how to constrain the use of global state. And for functional - in C.A.R. Tony Hoare's lecture on "The Billion Dollar Mistake", a guy stands up at the end with the message "Haskell is all fun and games until you invoke the I/O monad" :) > <snip> > >> For what it is worth, If I knew what I was trying to way, I'd say it :) >> > > OK. If you figure it out, we can take it up again - otherwise I think > any replies I'd make would add to the confusion (mine, yours, or > everyone else's). > It would be - in my opinion, we're obligated to do everything within our power to get things as close to correct as possible. And, for some reason, there isn't that much taught about how to do this, so we're probably on our own. But the fact remains that we must do this. This begins with design to provide information to help determine that things work as expected. It continues with spending time on frameworks, whether built or bought, to help check things. -- Les Cargill
[toc] | [prev] | [next] | [standalone]
| From | David Brown <david.brown@hesbynett.no> |
|---|---|
| Date | 2018-09-23 15:21 +0200 |
| Message-ID | <po841j$dlu$1@dont-email.me> |
| In reply to | #28100 |
On 22/09/18 20:50, Les Cargill wrote:
> David Brown wrote:
>> On 22/09/18 05:15, Les Cargill wrote:
>>> David Brown wrote:
>>>> On 18/09/18 04:24, Les Cargill wrote:
>>>>> David Brown wrote:
>>>>>> On 16/09/18 15:33, Tom Gardner wrote:
>>>>>>> On 16/09/18 14:00, David Brown wrote:
>>>>> <snip>
>>> So what you can to is find the meat of what is possible and do that.
>>>
>>> I must say - I am rather tired of this old warhorse; an appeal to
>>> Godel in the form of an economics question. All I would say is
>>> that you should test as well as you can. You should use a dragon to
>>> fight the dragon.
>>
>> No one will argue against the benefits of testing as well as you
>> reasonably can. Testing is often good enough to reach the level of
>> confidence you want for code.
>>
>> But you are simply /wrong/ to think that non-exhaustive testing can
>> somehow "prove" that code works.
>>
>
>
> "Proof" isn't that interesting outside of certain contexts. By "proof"
> I mean fully formal verification that it's 100% known to be correct.
>
> We want to find a break-even variation on that. We want the cost and
> the risk to be commensurate.
>
Agreed.
> Turns out, just measuring the risk is pretty hard.
>
Agreed.
>> And there are some classes of problem for which testing is extremely
>> unlikely to identify the problem. In particular, for anything
>> involving race conditions or timing, you cannot /test/ your way to
>> working code.
>
> Not in harness, but you can prove out the approach being used as a
> demonstration and reasoning tool. And it depend on the problem - you
> might be able to generate test vectors that get darned close.
>
> You point is probably "yes, but how close?" :) And it's a good one.
>
Exactly, yes.
Let's take an example of where people get things wrong. We have all
seen code like this:
// Make counter volatile so that it is atomic and safe for interrupts
// even though we have a 16-bit cpu
volatile uint32_t counter;
void timerInterrupt(void) {
counter++; // It's volatile - this is safe
}
uint32_t readCounterFromMainLoop(void) {
return counter; // It's volatile - reading is atomic
}
Hopefully everyone reading this thread knows what the author's
misunderstanding is here. Yet we have all seen code written this way.
How much testing do you need before you are likely to catch a problem here?
If the timer is run at 1000 Hz, you'll get a 16-bit overflow once per
minute. If you have something like a 10 MHz msp430 processor, you've
got maybe a 0.2 microsecond window where there is a danger while reading
the counter. Perhaps you read 100 times a second. That means you spend
1/50,000 of your time in the danger zone. So every minute, you have a
1/50,0000 chance of a disaster. If my sums are right, you'll have a 50%
chance of trouble after about 35,000 minutes - or 24 days. And that's
assuming the problem is immediately obvious.
You are /never/ going to catch this in any practical lab testing. But
if you sell 10,000 units, it /will/ occur in live installations.
So how close is your testing at showing the code is good? Absolutely
useless.
This is not an unrealistic example. And you don't even need something
this unlikely. Boeing made engine controllers that failed if they ran
for something like 600 days without a restart - no one could spot that
problem in testing. Microsoft's Win 95 crashed reliably after 49 days
when a 32-bit millisecond counter overran - it took /ten years/ to spot
the problem, despite the huge numbers of systems in use.
There are things in code that you simply have to get right - you
/cannot/ test that they are cocrect. (As others have said, you might
catch them with static analysis tools.)
> As an example, I had a "one producer/one consumer" buffer. I wasn't
> 100% sure if it needed semaphores - one producer, one consumer, right?
>
> I thought about it a bit , built a driver loop
> and was able to prove that I did indeed need semaphores. To be fair,
> I was leaning that way anyway.
>
Simplification of your structures and interactions can make it vastly
easier to figure out what is correct and what is not.
>> You have to write the code correctly in the first place, because the
>> chances of spotting the microsecond window of disaster in your lab
>> testing is tiny. (I am not saying you need to formally prove the code
>> - again, this is all about appropriate balances of time and effort -
>> but testing does not help.)
>>
>
> Maybe it's bias from seeing stuff online, but I get the feeling
> that many people ( and I'm pretty sure you, David, are not one of them )
> just sort of despair of the whole thing.
I am certainly not in despair! I am merely concerned when people
apparently think that good testing is all they need to be sure their
code works correctly.
>
>>
>>>
>>> And so if your system is adept at rejecting inputs it cannot expect,
>>> then what?
>>>
>>> It's all about the ability to enforce constraints. Sort your
>>> constraints by the ability to do damage.
>>>
>>>> A functional programming language like Haskell gives you a much better
>>>> chance of actually proving the correctness of your code than an
>>>> imperative language like C - that is one of the reasons for the
>>>> existence of functional programming languages (it is the lack of state
>>>> and side-effects that help). But if you want to prove the correctness
>>>> of your Haskell program, you do it by an analysis of the code, or by
>>>> deriving correct code in the first place - you don't do it by testing.
>>>>
>>>
>>> That's because we'd like to pretend that "analysis" is some
>>> process that's not automatable. Or, at least, not somehow aided by
>>> automation.
>>
>> Analysis is much easier when you have restrictions on what can happen.
>
> You said it man. :)
>
>> In a pure functional programming language, your function takes some
>> input and works solely on that input, and the only effect of the code
>> is to generate the output. That means you can analyse it in
>> isolation. In general C code, your function might use or change
>> global state - it all quickly becomes a lot more complicated.
>>
>
> But the thing you must learn with C is how to constrain the
> use of global state.
>
> And for functional - in C.A.R. Tony Hoare's lecture on "The Billion
> Dollar Mistake", a guy stands up at the end with the message "Haskell is
> all fun and games until you invoke the I/O monad" :)
>
That is the challenge with functional programming languages - for real
life code, you usually need some state!
>> <snip>
>>
>>> For what it is worth, If I knew what I was trying to way, I'd say it :)
>>>
>>
>> OK. If you figure it out, we can take it up again - otherwise I think
>> any replies I'd make would add to the confusion (mine, yours, or
>> everyone else's).
>>
>
>
> It would be - in my opinion, we're obligated to do everything within our
> power to get things as close to correct as possible. And, for some
> reason, there isn't that much taught about how to do this, so we're
> probably on our own. But the fact remains that we must do this.
>
Agreed.
> This begins with design to provide information to
> help determine that things work as expected. It continues with spending
> time on frameworks, whether built or bought, to help check things.
>
These points are true in themselves - but miss 90% of the more important
issues. If you leave the paragraph so unfinished, it gives entirely the
wrong impression.
[toc] | [prev] | [next] | [standalone]
| From | Tom Gardner <spamjunk@blueyonder.co.uk> |
|---|---|
| Date | 2018-09-23 16:06 +0100 |
| Message-ID | <3_NpD.295124$fy.290641@fx26.am4> |
| In reply to | #28112 |
On 23/09/18 14:21, David Brown wrote:
> On 22/09/18 20:50, Les Cargill wrote:
>> David Brown wrote:
>>> On 22/09/18 05:15, Les Cargill wrote:
>>>> David Brown wrote:
>>>>> On 18/09/18 04:24, Les Cargill wrote:
>>>>>> David Brown wrote:
>>>>>>> On 16/09/18 15:33, Tom Gardner wrote:
>>>>>>>> On 16/09/18 14:00, David Brown wrote:
>>>>>> <snip>
>
>>>> So what you can to is find the meat of what is possible and do that.
>>>>
>>>> I must say - I am rather tired of this old warhorse; an appeal to
>>>> Godel in the form of an economics question. All I would say is
>>>> that you should test as well as you can. You should use a dragon to
>>>> fight the dragon.
>>>
>>> No one will argue against the benefits of testing as well as you
>>> reasonably can. Testing is often good enough to reach the level of
>>> confidence you want for code.
>>>
>>> But you are simply /wrong/ to think that non-exhaustive testing can
>>> somehow "prove" that code works.
>>>
>>
>>
>> "Proof" isn't that interesting outside of certain contexts. By "proof"
>> I mean fully formal verification that it's 100% known to be correct.
>>
>> We want to find a break-even variation on that. We want the cost and
>> the risk to be commensurate.
>>
>
> Agreed.
>
>> Turns out, just measuring the risk is pretty hard.
>>
>
> Agreed.
>
>>> And there are some classes of problem for which testing is extremely
>>> unlikely to identify the problem. In particular, for anything
>>> involving race conditions or timing, you cannot /test/ your way to
>>> working code.
>>
>> Not in harness, but you can prove out the approach being used as a
>> demonstration and reasoning tool. And it depend on the problem - you
>> might be able to generate test vectors that get darned close.
>>
>> You point is probably "yes, but how close?" :) And it's a good one.
>>
>
> Exactly, yes.
>
> Let's take an example of where people get things wrong. We have all
> seen code like this:
>
> // Make counter volatile so that it is atomic and safe for interrupts
> // even though we have a 16-bit cpu
> volatile uint32_t counter;
>
> void timerInterrupt(void) {
> counter++; // It's volatile - this is safe
> }
>
> uint32_t readCounterFromMainLoop(void) {
> return counter; // It's volatile - reading is atomic
> }
>
> Hopefully everyone reading this thread knows what the author's
> misunderstanding is here. Yet we have all seen code written this way.
>
> How much testing do you need before you are likely to catch a problem here?
>
> If the timer is run at 1000 Hz, you'll get a 16-bit overflow once per
> minute. If you have something like a 10 MHz msp430 processor, you've
> got maybe a 0.2 microsecond window where there is a danger while reading
> the counter. Perhaps you read 100 times a second. That means you spend
> 1/50,000 of your time in the danger zone. So every minute, you have a
> 1/50,0000 chance of a disaster. If my sums are right, you'll have a 50%
> chance of trouble after about 35,000 minutes - or 24 days. And that's
> assuming the problem is immediately obvious.
>
> You are /never/ going to catch this in any practical lab testing. But
> if you sell 10,000 units, it /will/ occur in live installations.
>
> So how close is your testing at showing the code is good? Absolutely
> useless.
>
> This is not an unrealistic example. And you don't even need something
> this unlikely. Boeing made engine controllers that failed if they ran
> for something like 600 days without a restart - no one could spot that
> problem in testing. Microsoft's Win 95 crashed reliably after 49 days
> when a 32-bit millisecond counter overran - it took /ten years/ to spot
> the problem, despite the huge numbers of systems in use.
>
>
> There are things in code that you simply have to get right - you
> /cannot/ test that they are cocrect. (As others have said, you might
> catch them with static analysis tools.)
Just so.
And for another example, consider the Patriot missile failure:
http://www-users.math.umn.edu/~arnold/disasters/patriot.html
The other significant problem is developing good tests is
/at least/ as difficult as developing the application.
It is hard enough to get developers to write tests that
adequately test "happy days" (?daze?) normal operation.
Getting them to develop good tests for fault conditions
is more difficult.
Hell, many times they don't even /conceive/ of failure modes,
and /actively/ argue "that can't happen, the framework takes
care of it". Oh, so the framework has solved the Byzantine
General's problem, has it? And too many other examples.
[toc] | [prev] | [next] | [standalone]
| From | julio@diegidio.name |
|---|---|
| Date | 2018-09-23 08:41 -0700 |
| Message-ID | <ece589da-9139-4aaf-8810-7a45ec969a00@googlegroups.com> |
| In reply to | #28113 |
On Sunday, 23 September 2018 17:06:44 UTC+2, Tom Gardner wrote: > It is hard enough to get developers to write tests that > adequately test "happy days" (?daze?) normal operation. > Getting them to develop good tests for fault conditions > is more difficult. And beside the point anyway, while a (good) spec is supposed to cover all relevant cases to begin with: replied the developer. Good tests are a necessary condition for risk management, yet not by any stretch a sufficient condition to write quality code. Julio
[toc] | [prev] | [next] | [standalone]
| From | Tom Gardner <spamjunk@blueyonder.co.uk> |
|---|---|
| Date | 2018-09-23 16:49 +0100 |
| Message-ID | <ZBOpD.380767$8C.89273@fx25.am4> |
| In reply to | #28114 |
On 23/09/18 16:41, julio@diegidio.name wrote: > On Sunday, 23 September 2018 17:06:44 UTC+2, Tom Gardner wrote: > >> It is hard enough to get developers to write tests that >> adequately test "happy days" (?daze?) normal operation. >> Getting them to develop good tests for fault conditions >> is more difficult. > > And beside the point anyway, while a (good) spec is supposed to cover all > relevant cases to begin with: replied the developer. Good luck getting the customer to specify all the relevant fault conditions! You're ahead of the game if they have a good idea of what it should do in normal operation. :( > Good tests are a necessary condition for risk management, yet not by any > stretch a sufficient condition to write quality code. Yes. I've seen too many bad and inadequate tests.
[toc] | [prev] | [next] | [standalone]
| From | julio@diegidio.name |
|---|---|
| Date | 2018-09-23 08:56 -0700 |
| Message-ID | <568d47fe-319c-4472-9660-061d1e582ba8@googlegroups.com> |
| In reply to | #28115 |
On Sunday, 23 September 2018 17:49:17 UTC+2, Tom Gardner wrote: > On 23/09/18 16:41, julio@diegidio.name wrote: > > On Sunday, 23 September 2018 17:06:44 UTC+2, Tom Gardner wrote: > > > >> It is hard enough to get developers to write tests that > >> adequately test "happy days" (?daze?) normal operation. > >> Getting them to develop good tests for fault conditions > >> is more difficult. > > > > And beside the point anyway, while a (good) spec is supposed to cover all > > relevant cases to begin with: replied the developer. > > Good luck getting the customer to specify all the relevant > fault conditions! That's just not the customer's job! It's rather called (good) analysis: replied again the developer, though conscious of the decades of relentless demolition campaigns of analysis to begin with... i.e. of the very premise for doing any job properly (and for taking responsibility for results). > I've seen too many bad and inadequate tests. If that's your main problem, you haven't seen nearly enough... HTH (and EOD), Julio
[toc] | [prev] | [next] | [standalone]
Page 2 of 4 — ← Prev page 1 [2] 3 4 Next page →
Back to top | Article view | comp.arch.embedded
csiph-web