On 9/19/13 9:29 PM, josef.win...@email.de wrote:
Does OpenBSD plan to varify its (main) components, to
reach the level of zero-bug software?
I do assume that you are talking about "formal verification" meaning
"mathematical proof of correctness".
Verify against what? Verification is a binary
Running 5.3 (release) i386 on a soekris net4521 with 2 connected
sis(4). The device is a router/firewall on a home network with a cable
Internet connection. One of these interfaces has in the last few weeks
started to build higher rates of input errors as time increases
between reboots. This seems
On 09/17/2013 19:25, Predrag Punosevac wrote:
Internet (128.xxx) OpenVPN clients (VPN network 10.8.0.xxx)
|Also Public 128.xxx addresses
||
||
-
On Thu, Sep 19, 2013 at 21:41, Jonathan Thornburg wrote:
> # bioctl softraid1
> bioctl: Can't locate softraid1 device via /dev/bio
> and a quick grep through dmesg reveals only one softraid device
> (softraid0) mentioned.
>
> Question: What's the right way to have multiple independent softraid
>
I have an amd64 laptop (Thinkpad T60) whose /, /var, and /usr are
standard FFS partitions (dksklabel fstype 4.2BSD), while /home is
encrypted via softraid crypto: on boot I login as root, and run a perl
script which executes (with lots of error checking & optional logging)
# sd0 is the built-in d
There is a fuse implmentation, however as mentioned, it is rather slow.
It's main targets were reading ZFS volumes on Linux and OSX. It is also
rather outdated in favor of the native Linux port (abandoning OSX.) A
better starting point would be the FreeBSD port, but it will still
remain CDDL licens
I suspect one of the crashes has corrupted the filesystem holding your
cvs checkouts. I'd suggest newfs, restoring any important data on that
partition from backups, and re-fetching replaceable data (cvs checkouts
etc) from another source.
On 2013-09-19, Stefan Wollny wrote:
> Hi there, working
pe...@bsdly.net (Peter N. M. Hansteen) writes:
> systems that have developed in response to real-world needs and formal
> standards specifications that at least in some cases more likely than
> not were in any way verified even to be internally consistent.
missing a 'never' in there. clearer?
-
josef.win...@email.de writes:
> Right, a varified full flaged OS is still future.
> But there is nevertheless progress and affort.
Thanks for the pointeres, but anytime this comes up, an old AI
witticism turns up at the back of my head,
"If our mind were so simple we could actually u
On Thu, Sep 19, 2013 at 2:44 PM, Stefan Wollny wrote:
> I have this ancient IBM/lenovo T60 with me while working off-site. This
> machine used to be a reliable workhorse until recently. Since roughly around
> the time of the ABI changes to 64-bit time I get annoyed by 2~3 crashes per
> day. I u
Mihai Popescu wrote:
> > "An Analysis of Data Corruption in the Storage Stack"
> > http://www.cs.toronto.edu/~bianca/papers/fast08.pdf
>
> They claim the paper is based on 1.53 million disk drives.
> It is interesting they were able to access such a number.
The paper is based on NetApp data.
-
Hi Philip,
thank you for taking the time to reply: Of course, you are 100% right - without
proper crash reports such complaints are rather useless. But I cannot describe
a reproduceabel situation that leads to a crash. The only common circumstance
is that the crashes occured when running X. Un
On Thu, Sep 19, 2013 at 11:44:20PM +0200, Stefan Wollny wrote:
> Send a second time as this webmail-programm changed to HTML again...
> this mail should be better to read.
>
> Hi there,
>
> I have this ancient IBM/lenovo T60 with me while working off-site. This
> machine used to be a reli
On Thu, Sep 19, 2013 at 11:49:56PM +0300, Mihai Popescu wrote:
| > Since I mentioned the likelihood of a non-recoverable disk error,
| > here's a terrific paper that should make everbody sleep very poorly:
| >
| > "An Analysis of Data Corruption in the Storage Stack"
| > http://www.cs.toronto.edu/~
Hi there, working off-site for a few days I took my ancient IBM/lenovo
T60 (i386 - bsd.mp) with me. Two days ago I upgraded to the latest
snapshot, #61 as of September, 17th, from openbsd.cs.fau.de. (dmesg at
the end) Tonight I updated /usr/src via cvs. It appeared to me that a
whole copy of /usr w
On 09/20/13 00:00, thornton.rich...@gmail.com wrote:
Interesting thread...
Sent from my BlackBerry 10 smartphone on the Verizon Wireless 4G LTE
network.
this is misc@, not twitter.
while i finally reply to message by you, i want to ask a question.
how about dropping at least the 'Wireless' out
> Since I mentioned the likelihood of a non-recoverable disk error,
> here's a terrific paper that should make everbody sleep very poorly:
>
> "An Analysis of Data Corruption in the Storage Stack"
> http://www.cs.toronto.edu/~bianca/papers/fast08.pdf
They claim the paper is based on 1.53 million d
Send a second time as this webmail-programm changed to HTML again... this
mail should be better to read.
Hi there,
I have this ancient IBM/lenovo T60 with me while working off-site. This machine
used to be a reliable workhorse until recently. Since roughly around the time
of the ABI chan
On 09/19/2013 04:29 PM, josef.win...@email.de wrote:
Does OpenBSD plan to varify its (main) components, to
reach the level of zero-bug software?
you mean, painfully reviewing and auditing code?
what do you think they've been trying to do for the last 15 years?
And after that, they have been try
On Thu, Sep 19, 2013 at 22:29, josef.win...@email.de wrote:
> Does OpenBSD plan to varify its (main) components, to
> reach the level of zero-bug software?
>
> If not, isn't there any concern that (future) varified OS
> will render OBSD redundant one day?
Short answer: no. Long answer: still no.
On Thu, Sep 19, 2013 at 10:29:39PM +0200, josef.win...@email.de wrote:
> Does OpenBSD plan to varify its (main) components, to
> reach the level of zero-bug software?
No. Zeno convinced us that you can't get there from here.
>
> If not, isn't there any concern that (future) varified OS
> will re
Hi there, I have this ancient IBM/lenovo T60 with me while working
off-site. This machine used to be a reliable workhorse until recently.
Since roughly around the time of the ABI changes to 64-bit time I get
annoyed by 2~3 crashes per day. I usually run OpenBSD's latest snapshots
on it and I can co
On Thu, Sep 19, 2013 at 05:14:37PM -0400, Nick Holland wrote:
> Don't get me wrong, I'd love to see a general purpose OS with the
> basic reliability of my car,
Actually, it looks more and more like the reverse is coming true.
josef.win...@email.de writes:
> Does OpenBSD plan to varify its (main) components, to
> reach the level of zero-bug software?
>
> If not, isn't there any concern that (future) varified OS
> will render OBSD redundant one day?
I remain unconvinced that it's possible to formally verify non-trivial
Interesting thread...
Sent from my BlackBerry 10 smartphone on the Verizon Wireless 4G LTE
network.
From: josef.winger@email.deSent: Thursday, September 19, 2013 4:30 PMTo:
misc@openbsd.orgSubject: Verified OS concerns
Does OpenBSD plan to varify its (main) components, to
reach the level of zero-
Since I mentioned the likelihood of a non-recoverable disk error,
here's a terrific paper that should make everbody sleep very poorly:
"An Analysis of Data Corruption in the Storage Stack"
http://www.cs.toronto.edu/~bianca/papers/fast08.pdf
--
Christian "naddy" Weisgerber
On Thu, Sep 19, 2013 at 01:46:20PM +, hru...@gmail.com wrote:
> Raimo, if people believe that hash(A)=hash(B) implies A=B, so strong
> believe, that they use it in their programs,
It's a matter of engineering. Usually that is good enough.
If you don't think it's good enough then you should pr
Does OpenBSD plan to varify its (main) components, to
reach the level of zero-bug software?
If not, isn't there any concern that (future) varified OS
will render OBSD redundant one day?
/jo
On 09/19/2013 08:46 AM, hru...@gmail.com wrote:
From time to time I think I should follow Kenneth Westerbacks
recomendation
and go to a math-for-idiots list, for example to Usenet Group
"sci.math",
and then make a link to this thread in gmane: they will sure admire
Marc
Espies wisdom and his
On Thu, Sep 19, 2013 at 8:44 PM, Jiri B wrote:
> Because it was Isreali Qumranet which was developing
> KVM a lot and tools around and which was then bought
> by Red Hat.
http://en.wikipedia.org/wiki/Moshe_Bar_%28investor%29
On Wed, September 18, 2013 6:28 pm, Kapetanakis Giannis wrote:
> I've just came on this:
> http://mailman.cs.huji.ac.il/pipermail/linux-il/2013-September/010649.html
>
> Just a short quote of it:
> "Hi, today we've made the first release of OSv, a new operating system
> for running applications on
On Thu, Sep 19, 2013 at 10:50:16AM -0700, latin...@vcn.bc.ca wrote:
> On Wed, September 18, 2013 6:28 pm, Kapetanakis Giannis wrote:
> > I've just came on this:
> > http://mailman.cs.huji.ac.il/pipermail/linux-il/2013-September/010649.html
> >
> > Just a short quote of it:
> > "Hi, today we've made
2013/9/19 Stuart Henderson
> On 2013-09-19, MERIGHI Marcus wrote:
> > Other obvious suggestions: HENQ, NEWQ, PQ
>
> pff, the old one was ALTQ, clearly this should be NEUQ ;)
>
>
NEUQ sound like a region from Argentina: Neuquén
fair for the german, it is not zen tough
NEUQ, like NUKE ?
i vote for TheQueue, because What else ?!
On Thu, Sep 19, 2013 at 9:14 AM, Stuart Henderson wrote:
> On 2013-09-19, MERIGHI Marcus wrote:
> > Other obvious suggestions: HENQ, NEWQ, PQ
>
> pff, the old one was ALTQ, clearly this should
On 09/19/2013 04:18 PM, Stuart Henderson wrote:
On 2013-09-19, Gregory Edigarov wrote:
I've connected it to Windows via USB, and installed software which
came with it, snooped the protocol, and I am dead sure it is an old and
frayed Megatec/Q1, which should work with blazer_usb driver from nut.
Raimo Niskanen wrote:
> Rodrigo,
>
> was there anything wrong with my answer below (and others equal),
> apart from it not being the one you wanted, since you keep repeating
> the same question over and over again?
>
> Do you have a better answer? Please share it for us to check.
Raimo, if peop
On 2013-09-19, Gregory Edigarov wrote:
> I've connected it to Windows via USB, and installed software which
> came with it, snooped the protocol, and I am dead sure it is an old and
> frayed Megatec/Q1, which should work with blazer_usb driver from nut.
> But it isn't. Seems I've tried nearly ever
On 2013-09-19, Martin Pieuchot wrote:
> nut depends on the libusb to talk to the ups, and to be fully
> functional with the libusb your device must be attached to
> ugen(4). That's why usb_quirks.c contains various UPS.
Actually, NUT is perfectly happy with many UPS attached to uhid
and I think
On 2013-09-19, MERIGHI Marcus wrote:
> Other obvious suggestions: HENQ, NEWQ, PQ
pff, the old one was ALTQ, clearly this should be NEUQ ;)
Rodrigo,
was there anything wrong with my answer below (and others equal),
apart from it not being the one you wanted, since you keep repeating
the same question over and over again?
Do you have a better answer? Please share it for us to check.
On Tue, Sep 17, 2013 at 03:58:34PM +0200, Raimo
> This part:
>
>> VOP_FSYNC() at VOP_FSYNC+0x2f
>> ffs_sync_vnode() at ffs_sync_vnode+0x77
>> vfs_mount_foreach_vnode() at vfs_mount_foreach_vnode+0x38
>> ffs_sync() at ffs_sync+0x83
>> sys_sync() at sys_sync+0xa1
>> vfs_syncwait() at vfs_syncwait+0x50
>> vfs_shutdown() at vfs_shutdown+0x32
>> boot
I want to give a hint for those working till now in the problem of
estimating the probability of A=B under the condition of hash(A)=hash(B).
Just suppose that hash is any function from a set X to Y, first suppose
that X is finite (but very big), and that the probability to pick any
element is the
My vote -> *HENQ
Chickens lined up..
On Thu 19 Sep 2013 11:34:03 BST, MERIGHI Marcus wrote:
pkesh...@gmail.com (patrick keshishian), 2013.09.19 (Thu) 09:39 (CEST):
On Thursday, September 19, 2013, Ted Unangst wrote:
On Thu, Sep 19, 2013 at 09:14, Henning Brauer wrote:
*ALTQ's replacement..
D
On 19 September 2013, Gregory Edigarov wrote:
> On 09/19/2013 12:20 PM, Gregory Edigarov wrote:
> >Hello, everybody.
> >
> >A few days ago I've bought a new ups, as a replacement for my old
> >one, which got it's last way to junkyard. The old one had RS232
> >, and the new one is an USB u
pkesh...@gmail.com (patrick keshishian), 2013.09.19 (Thu) 09:39 (CEST):
> On Thursday, September 19, 2013, Ted Unangst wrote:
> > On Thu, Sep 19, 2013 at 09:14, Henning Brauer wrote:
> > >> *ALTQ's replacement..
> > >> Does it have a name yet, or are you sticking with; new super duper
> > >> simple
On 09/19/2013 12:20 PM, Gregory Edigarov wrote:
Hello, everybody.
A few days ago I've bought a new ups, as a replacement for my old one, which
got it's last way to junkyard.
The old one had RS232 порт, and the new one is an USB ups.
Trying different ways to connect it to OpenBSD, but everythin
On 19/09/13(Thu) 12:20, Gregory Edigarov wrote:
> Hello, everybody.
>
> A few days ago I've bought a new ups, as a replacement for my old one, which
> got it's last way to junkyard.
> The old one had RS232 порт, and the new one is an USB ups.
> Trying different ways to connect it to OpenBSD, but
On Thu, Sep 19, 2013 at 12:20:14PM +0300, Gregory Edigarov wrote:
> Hello, everybody.
>
> A few days ago I've bought a new ups, as a replacement for my old one, which
> got it's last way to junkyard.
> The old one had RS232 порт, and the new one is an USB ups.
> Trying different ways to connect
Hello, everybody.
A few days ago I've bought a new ups, as a replacement for my old one, which
got it's last way to junkyard.
The old one had RS232 порт, and the new one is an USB ups.
Trying different ways to connect it to OpenBSD, but everything I've tried fails.
The UPS reports itself as:
u
> Personally, I'm an long time fvwm user. My partner wouldn't know where to
> start nor care to learn how to use that. Which is why I need to install a DE.
> Years ago I did use KDE3 and liked it but changed because I did not like KDE4.
Don't forget especially with xfce you can take just parts o
On Thursday, September 19, 2013, Ted Unangst wrote:
> On Thu, Sep 19, 2013 at 09:14, Henning Brauer wrote:
>
> >> *ALTQ's replacement..
> >>
> >> Does it have a name yet, or are you sticking with; new super duper
> >> simple prio queuer?
> >
> > I'm not into marketing. It's just the new queueing s
On Thu, Sep 19, 2013 at 09:14, Henning Brauer wrote:
>> *ALTQ's replacement..
>>
>> Does it have a name yet, or are you sticking with; new super duper
>> simple prio queuer?
>
> I'm not into marketing. It's just the new queueing subsystem.
JTNQ it is, then.
* Andy [2013-09-17 15:36]:
> On Tue 17 Sep 2013 13:48:45 BST, Stuart Henderson wrote:
> >On 2013-09-16, Andy wrote:
> >>Planning to test Hennings new ALTQ subsystem diff on OpenBSD 5.4 with
> >>this hardware :D
> >pardon the pedantry, but it's not altq..
> Lol, yes sorry ;)
>
> *ALTQ's replaceme
53 matches
Mail list logo
