<kyak>
yeah, this exact notion of "proper OS" had been preventing me from using Linux on desktop for many years
<whitequark>
didn't prevent me, but it's just not good design. or should I say, lack of any design whatsoever?
<whitequark>
neither unix nor c were ever designed; they went from "kept together with wd-40 and duct tape" to "the committee decides where do we add more wd-40 and duct tape"
<whitequark>
and if you dare to tear off even the tiniest chunk of the duct tape, the whole contraption folds
<whitequark>
I'm not even exaggerating
<kyak>
so you just went blaming from unix to c, good move :)
<whitequark>
well, they're tightly related. and suggesting unix as an example of proper... anything is absurd
<whitequark>
practically everything else that exists is just even more horrible, though
<kyak>
that's what i was going to say.. there is no "proper"
<whitequark>
there is "proper", deep within research labs and the like
<whitequark>
sadly, software, especially free software, is governed by network effects, not quality
<kyak>
sometimes the research labs are even more far away from proper, untied to real life and real application
<whitequark>
some of them are, some of them are far more practical than anything the industry offers
<whitequark>
how about, I dunno, a JavaCard with a sandbox that is mathematically proven to be impenetrable?
<kyak>
50 years after, somebody proves that your mathematics is wrong
<whitequark>
not going to happen.
<kyak>
and laughs at "shitty design"
<whitequark>
you still have to care about a bunch of other kinds of attacks, say, side-channel attacks allowing to extract key material
<kyak>
well, designers of unix definitely had no idea you wanted you flash drive mount automatically
<whitequark>
but at least a random guy from the street can't execute and persist any code he likes on your "secure" container
<kyak>
new technologies arise, making older designs obsolete. You can't account for everything
<whitequark>
design of unix was outdated right when it has appeared, and not too far long in the future everyone just started adding silly extensions
<kyak>
i'm not sure about that..
xiangfu has joined #qi-hardware
<whitequark>
about what, unix wars or that it was broken from the start?
<kyak>
that unix was outdated right when it appeared
<whitequark>
take a look at ALGOL-68 and Burroughs B5000, for example
<whitequark>
and that wasn't exactly rocket science at the point
pcercuei has joined #qi-hardware
<whitequark>
if you think unix is somehow innovative in timesharing, virtual memory, etc, etc, just take a look at the design of THE multiprogramming system
<kyak>
there is no "good" and "evil", i'm pretty sure what you mentioned had its drawbacks. There is a reason unix survived
<whitequark>
that reason is not technical. it's called "network effects"
<kyak>
i doubt that
<whitequark>
well, it's easy to eliminate technical reasons. you just have to look at the design of contemporary systems
<whitequark>
so when you eliminate the impossible, the rest, however doubtful, must be the truth
<kyak>
i prefer to believe in natural selection.. the better survices, the worse dies
<kyak>
if unix survived, and nobody knows about Burroughs B5000, than unix is better - easy.
<whitequark>
more fit ≠ technically better. exactly what I'm telling you about.
<kyak>
well, this just proves that fitness is not all about technical greatness
<whitequark>
and there's nothing good about that
<whitequark>
fitness considers immediate, short-term gain, usually sacrificing long-term one
<kyak>
don't even talk about long term in this area...
<whitequark>
do I have to point you to the amount of idiotic vulnerabilities in software written in C?
<whitequark>
do I have to remind you that today, practically any system is vulnerable if poked just a little bit harder than usual?
<whitequark>
do I have to explain that this does not have to be the case?
<kyak>
do i have to point out that C language is all about trade off?
<kyak>
the tools is more dangerous, but allows to do more
<kyak>
and sometimes more efficiently
sb0 has joined #qi-hardware
<kyak>
if you don't like it, choose another tool
<whitequark>
I can't, that's the whole problem
<whitequark>
all the OSes are written in C. my bank uses C. my hospital uses C. the thing in my pocket that has all the information about me uses C. so on.
<kyak>
then the time for the "new" tool can not come yet
<whitequark>
so you're saying, ummmm, "C is good because network effects prevent adoption of anything else".
<whitequark>
that's amazing logic, I can use it to justify anything
<kyak>
when people reached the limits of wooden tools, then invented how to used stone tools
<kyak>
so it seems like C yet has something to say
<whitequark>
and talking about the tradeoffs... it's basically a UI failure. C makes it very easy to write dangerously incorrect code
<whitequark>
it could make that hard, but didn't. thus, bad design.
<whitequark>
when your cars trap people inside on collisions and catch fire, you don't say "that's a design choice", whether it was one. you recall the damn cars and make sure this never happens again
<whitequark>
but I guess the field will be so immature until most of the people who think suck tooling is OK die.
<kyak>
that's why none of automotive companies writes C code by hand anymore :)
<whitequark>
of course they do, MISRA-C is explicitly targeted at handwritten C code
<kyak>
have you heard of MISRA-AC-AGC?
<whitequark>
how widely is it deployed?
<kyak>
don't get me started about automatic code generation, i've been in the automotive industry for years
viric_ has joined #qi-hardware
<whitequark>
and anyway, automotive even has it relatively good. consumer is where the horror truly lies
<whitequark>
I grant you that automotive, or aerospace, are able to deal with the fallout (but at what cost?)
<kyak>
..and ACG is used very widely
<whitequark>
now look at openssl
<kyak>
yeah, thats another story
<whitequark>
or linux--local privilege escalation is so often, people don't even talk about it a lot
<kyak>
they should learn the lesson: "everyone needs formal verification"
<whitequark>
kyak++
<whitequark>
have you seen Coq?
<larsc>
its funny. A lot of companies now want to use Linux in the automotive segement, but the Linux kernel coding sytle clashes with the MIRSA coding style.
<whitequark>
or CompCert?
<kyak>
nope, i've seen Polyspace
<whitequark>
absolutely do take a look at CompCert. it's a formally verified C compiler that optimizes code at about GCC's -O1
<whitequark>
meaning there can be no miscompilation.
viric has quit [Ping timeout: 245 seconds]
viric_ is now known as viric
<whitequark>
there's the issue of verifying the code itself, but it's another one :)
<kyak>
intersting.. then you have a look at Polyspace, it's a formal verification tool (using abstract interpretation) that works on C/C++/Ada code
<whitequark>
I will. have you also seen KLEE?
<kyak>
i wonder how CompCert goes about DO-178 qualification...
<kyak>
nope
<whitequark>
that's LLVM's abstract interpreter
<whitequark>
DO-178 is one of the goals for CompCert development, yes. no idea if they actually got the papers
<kyak>
it's a big pain in the industry, actually.. the lack of qualified compiler
<whitequark>
ha
<kyak>
and the companies do weird things to prove their object code is correct to source code...
<whitequark>
seems you need to cooperate with your friends from academia a bit more ;)
<kyak>
well.. there will always be a gap between research and development
<kyak>
whitequark: please point me to KLEE, google shows irrelevant results
<whitequark>
but it's a huge pain in the ass to deal with, unfortunately
<whitequark>
like, I've spent six hours yesterday trying that my Peano-representation-to-binary-digits converter is correct, which is probably one of the most basic things you could imagine
<whitequark>
I failed
<whitequark>
trying to prove*
<kyak>
whitequark: btw, there are tools that let you automatically generate tests for 100% model coverage (the model, from which the code is generated). It uses formal methods, so 100% coverage is guaranteed (unless there is "dead code", which you then automagically find)
<whitequark>
what about dynamical invariants?
<kyak>
what's that?
<kyak>
like, polymorphism?
<whitequark>
hrm, no. something like "if(fuel_low && fuel_high) {", that can't ever be dynamically true, but there's no way to statically infer that
<whitequark>
how would your tool handle it?
<whitequark>
I'm not talking about the case when there's two sensors for fuel_low and fuel_high; that's just the differently interpreted output from a single sensor.
<kyak>
ah, it would prove it unsatisfiable
<whitequark>
as expected; and what'd you do?
<kyak>
the toos would show it to you, it is you, the developer, who needs to justify
<kyak>
the tools knows nothing about the physics behind the system, just the mathematics..
<whitequark>
well, nevermind, actually. the regulations usually dictate a highly restricted style of programming anyway
<whitequark>
what I mean is that such tools are OK for some limited areas, but for other places rapidly become inapplicable
<whitequark>
you can verify an L4 microkernel, say (it has been done), but there probably will not be a verified kernel for desktops for decades
<whitequark>
it's just too complex
<kyak>
these tools are good for algorithms, that is, the application software. It is indeed very hard to apply to system software
<kyak>
or basic software, if you wish
<whitequark>
there are still ways to gain confidence in the behavior of the overall system, namely split the system into smallest components with least authority and prove that the part that communicates messages is correct
<whitequark>
(the microkernel approach, if you'd like)
<whitequark>
e.g. this has been done to get a "verified" browser, where Webkit is ran in an OS sandbox, and only the controlling part is verified
<whitequark>
but they require a radical change in the software architecture, which is even less likely to happen than switch from C or something
<kyak>
and probably radical changes in minds..
<whitequark>
well, that's exactly the problem :)
<whitequark>
convince people that formal verification is good. then, convince them it's possible. then, convince they should invest in it.
<whitequark>
I've never heard of static data race analysis, to be honest
<larsc>
I was thinking about first splitting the code into blocks of sideeffect free code, then build a graph of which block may follow after which other block. But I'm afraid there will be a state explosion
<whitequark>
indeed
<whitequark>
you can probably split them into ranges or sets somehow
<whitequark>
I'm sure there's been literature on the topic, have you looked?
<larsc>
no, just had the thoughts a couple of hours ago
<larsc>
hm, what can run concurrent with what else typically only changes when you add/remove a new concurrent function to the system, or if you take/release a lock
<whitequark>
I can't parse that sentence
<larsc>
when you have two functions f1 and f2 and the can run concurrently that means that any instruction in f1 can be followed by any instruction in f2 and vice versa
<whitequark>
umm, that's a very simplified view
<whitequark>
I think you must consider a memory model
<whitequark>
larsc: really though, you don't need to consider all instructions
<whitequark>
you only need to ensure that concurrent access is either atomic or protected by a lock
<larsc>
yes, thats why I said split things into blocks of side-effect freeness
<whitequark>
no, I mean, you don't have to analyze all possible parallel paths at all
<whitequark>
concurrent paths, rather
<whitequark>
you only have to analyze a single path, because the predicate "protected by a lock" only considers a single thread
<whitequark>
("atomic" is trivial)
<larsc>
typically there is no global lock
<whitequark>
so you will have to categorize data into two categories: 1) owned by a thread T 2) protected by lock L
<whitequark>
then, for category 2, you'll have to prove that no accesses outside a section protected by a lock happen. this is a relatively simple flow analysis
<whitequark>
for 1, it's much trickier
<whitequark>
but I hope that kernel has some sane standard notion of ownership
<whitequark>
and there should never be any data that is neither owned by a specific thread nor protected by a lock
<whitequark>
makes sense?
<larsc>
yes
<larsc>
but I think it might be more complex
<whitequark>
I will happily discuss it; I'm fairly interested in the topic
<whitequark>
tbh I think you may be onto something; I can't recall any existing tools that work like that
* larsc
too, but I'm trying to get work done right now ;)
<larsc>
What I meant was that there are other ways of mutal exclusion then just taking a lock
<larsc>
e.g. before you register your callback ops you know that data accessed before that point can not be concurrently accessed in the callbacks
<whitequark>
that's ownership
<whitequark>
i.e. you can skip locking if you own the thing. but you're right in that now that becomes modal
<larsc>
I think I would describe it with code paths being dead or alive
<larsc>
there are certain events that mark a code path dead or alive
<larsc>
e.g. a taking a mutex makes all other codepaths that use the same mutex dead
<larsc>
you get in problems though when the calculation whether the code is dead or alive becomes turing complete
<whitequark>
yes, that's why I suggested ownership
<larsc>
e.g. if (rand() % 2) mutex_lock()
<whitequark>
ownership usually corresponds to some well-defined domain concept
<whitequark>
which people won't mess with just for the sake of maintainability
<whitequark>
say, memory allocated on stack is only owned by the caller
<whitequark>
memory allocated with malloc is owned by caller unless put into memory that belongs to someone els
<whitequark>
and you rarely if at all transfer ownership entirely
<whitequark>
perhaps only for something like buffers in a network stack
<larsc>
can you transfer ownership to None?
<larsc>
e.g. every thread needs to take a lock?
<whitequark>
sure, though I would call that "Shared"
<larsc>
ok
<whitequark>
it's basically a standard poisoning scheme
<whitequark>
larsc: frama-c.com?
<whitequark>
I'm being told it does what you want
atommann__ has quit [Ping timeout: 264 seconds]
porchao has quit [Ping timeout: 264 seconds]
porchao has joined #qi-hardware
atommann__ has joined #qi-hardware
<larsc>
I'll take a look, thanks
<viric>
many years ago, there was a tool called 'spin' or so
<wpwrak>
(spin) "still used" and why not ? it's a great tool
atommann__ has quit [Quit: Leaving]
<viric>
last time I touched it, it was in early 0s
<viric>
and back then I thought I was using an old tool
<wpwrak>
well, unless you design protocols for a living it's not a tool you should need every day ... ;-)
<viric>
I coulnd't find any other tool that did that, though
valhalla_ is now known as valhalla
<viric>
open source tool I mean
<wpwrak>
whitequark: (etchant comparison) not terribly useful, given that they only tried two
<whitequark>
mmm yes, it's only mildly interesting
<whitequark>
I definitely should try FeCl3-with-a-sponge
<whitequark>
seems to produce fascinating results. I'm not sure why *exactly* is it faster
<wpwrak>
FeCl is just a mess. have you ever tried it ? all the lovely stains ...
<whitequark>
I totally did
<whitequark>
had a 1L bottle of FeCl3 and used it for ~6 months
<wpwrak>
and you still want to go back to *that* ? :)
<whitequark>
it didn't really bother me in the ways you describe
<whitequark>
it was somewhat slow and uneven, but some of that can be attributed to poor tradecraft back then
<whitequark>
I don't ever want to deal with hot FeCl3 though
xiangfu has quit [Remote host closed the connection]
<wpwrak>
oh, it "works". but you need to warm it, any spills cause stains (and the messy procedure means that spills are more likely), it very quickly loses transparency, and it's a pain to get rid of the spent acid.
<whitequark>
just pour it down the drain
<wpwrak>
compare to HCl+H2O2: works fine at room temperature, very low spill risk and spills are colorless (i assume - haven't actually had one i noticed yet), stays clear all the way, you just let it dry and then dispose of the salt.
<whitequark>
(transparency) is it ever transparent?
<wpwrak>
in russia, there are no fish :)
<whitequark>
and acquiring H2O2 is still a pain...
<whitequark>
eh. as if a whopping 10g of copper would affect *anything*
<wpwrak>
fecl ? well, sufficient to see the pcb. but when etching starts, it all gets black
<whitequark>
and 10g of copper is how many pcbs? a hundred?
<wpwrak>
how big are your pcb ? and what sort of copper coating do you have ? 1/2 oz, 1 oz, 2 oz ? single-or double-sided ?
<whitequark>
say 1/2oz double-sided, 10x10cm would be most common
<whitequark>
and I usually pour the copper in planes on the board
<wpwrak>
so let's say 70% coverage
<whitequark>
fine
<wpwrak>
that should be about 1 gram of dissolved copper per board
<nicksydney>
wpwrak: you can make few boards and sell it on tindie ... surely people will buy it
<wpwrak>
wish we had less of a "you should do/make/..." culture here and more "i'll do/make/..."
<wpwrak>
idea, proof of concept design, etc., all there. neatly pre-chewed for someone else to continue with. but no. guess the couch is just too comfty :)
<nicksydney>
"i'm making RA8875 board" :)
<nicksydney>
and soon "I'm making scrollable LED for backpack"
<nicksydney>
wow the antocha design is nice
<nicksydney>
do you have pic of the proto for antorcha ?
<wpwrak>
it's aim for rigidity. mechanical stress on that thing is already through the roof, so anything that helps to keep chips from popping off the circuit is hotly welcome
<larsc>
then host->base = devm_ioremap_resource(&pdev->dev, host->mem_res)
<larsc>
the compiler should have actually screamed at your for that line
<apelete>
larsc: he didn't, kept the scream for himself :-/
<apelete>
I'll fix the lines you're talking about and try again
pcercuei is now known as zdrnk
<apelete>
larsc: gdb won't let me print the content of host->mem_res in mmc_probe callback: http://paste.debian.net/98532/
<apelete>
larsc: src_addr looks ok, but dma still fails (and dma_complete still isn't called) -> http://paste.debian.net/98533/
<apelete>
(gdb) p src_addr
<apelete>
$4 = 268570680
<apelete>
(gdb) p dst_addr
<apelete>
$5 = 14617216
<larsc>
we'll get there
<larsc>
dst_addr looks a bit short
<larsc>
you don't seem to set JZ_MMC_CMDAT_DMA_EN
<apelete>
hmm, not sure what you're talking about, let me look at the code
<larsc>
you need to set the JZ_MMC_CMDAT_DMA_EN in the CMDAT register, otherwise the MMC controller will not tell the DMA controller that there is any data to transfer
<larsc>
no data to transfer -> no callback
<apelete>
okay I see, so I should set JZ_MMC_CMDAT_DMA_EN in jz4740_mmc_send_command()