Model checking for highly concurrent code
Applied formal methods in order to test distributed systems — specifically GlusterFS:
I’ll use an example from my own recent experience. I’m developing a new kind of replication for GlusterFS. To make sure the protocol behaves correctly even across multiple failures, I developed a Murphi model for it. […] I added a third failure [to the simulated model]. I didn’t expect a three-node system to continue working if more than one of those were concurrent (the model allows the failures to be any mix of sequential and concurrent), but I expected it to fail cleanly without reaching an invalid state. Surprise! It managed to produce a case where a reader can observe values that go back in time. This might not make much sense without knowing the protocol involved, but it might give some idea of the crazy conditions a model checker will find that you couldn’t possibly have considered. […] So now I have a bug to fix, and that’s a good thing. Clearly, it involves a very specific set of ill-timed reads, writes, and failures. Could I have found it by inspection or ad-hoc analysis? Hell, no. Could I have found it by testing on live systems? Maybe, eventually, but it probably would have taken months for this particular combination to occur on its own. Forcing it to occur would require a lot of extra code, plus an exerciser that would amount to a model checker running 100x slower across machines than Murphi does. With enough real deployments over enough time it would have happened, but the only feasible way to prevent that was with model checking. These are exactly the kinds of bugs that are hardest to fix in the field, and that make users distrust distributed systems, so those of us who build such systems should use every tool at our disposal to avoid them.
(tags: model-checking formal-methods modelling murphi distcomp distributed-systems glusterfs testing protocols)
Is Trypophobia a Real Phobia? | Popular Science
ie. “fear of small, clustered holes”. Sounds like it’s not so much a “phobia” as some kind of innate, visceral disgust response; I get it. ‘As for who actually made the word up, that distinction probably belongs to a blogger in Ireland named Louise, Andrews says. According to an archived Geocities page, Louise settled on “trypophobia” (Greek for “boring holes” + “fear”) after corresponding with a representative at the Oxford English Dictionary. Louise, Andrews and trypophobia Facebook group members have petitioned the dictionary to include the word. The term will need to be used for years and have multiple petitions and scholarly references before the dictionary accepts it, Andrews says. I, for one, would prefer to forget about it forever.’
(tags: disgusting revulsion fear phobias trypophobia holes ugh innate)
Common phobia you have never heard of: Fear of holes may stem from evolutionary survival response
“We think that everyone has trypophobic tendencies even though they may not be aware of it,” said Dr Cole. “We found that people who don’t have the phobia still rate trypophobic images as less comfortable to look at than other images. It backs up the theory that we are set-up to be fearful of things which hurt us in our evolutionary past. We have an innate predisposition to be wary of things that can harm us.”
(tags: trypophobia holes fear aversion disgust ugh evolution innate)