Linked by martini on Tue 23rd Oct 2012 22:02 UTC
X11, Window Managers Wayland 1.0 was officialy released on October 22. Wayland is a protocol for a compositor to talk to its clients as well as a C library implementation of that protocol. The compositor can be a standalone display server running on Linux kernel modesetting and evdev input devices, an X application, or a wayland client itself. The clients can be traditional applications, X servers (rootless or fullscreen) or other display servers.
Thread beginning with comment 539813
To view parent comment, click here.
To read all comments associated with this story, please click here.
RE[5]: Comment by stabbyjones
by hackus on Wed 24th Oct 2012 04:14 UTC in reply to "RE[4]: Comment by stabbyjones"
hackus
Member since:
2006-06-28

Reminds me of the crap research I had to sit through where someone was trying to convince everyone you can mathematically prove a program and make it bug free.

What a gigantic load of crap.

-Hack

Reply Parent Score: 0

lucas_maximus Member since:
2009-08-18

Err well that is called Formal Specification.

http://en.wikipedia.org/wiki/Formal_methods

In some ways it is similar to unit testing except much more rigorous.

Edited 2012-10-24 10:20 UTC

Reply Parent Score: 4

RE[6]: Comment by stabbyjones
by Alfman on Wed 24th Oct 2012 16:37 in reply to "RE[5]: Comment by stabbyjones"
Alfman Member since:
2011-01-28

hackus,

"Reminds me of the crap research I had to sit through where someone was trying to convince everyone you can mathematically prove a program and make it bug free.
What a gigantic load of crap."

Not at all, if a program has a limited number of states, and each one of those states can be proven to do what is intended under all possible conditions, then you've got yourself a bug free program.

There's one huge caveat, a program has no choice but to assume its foundation (language and operating system) is bug free and deterministic. Alas, sometimes operating systems do break promises, in which case even "bug free" programs can behave unexpectedly.

Here's an example:

void*a=malloc(1000000);
if (a==null) exit(1); // exit predictably rather than crash
memset(a,0,1000000); // segfault?


This code can crash under linux because linux will allocate virtual memory addresses without ensuring there are sufficient physical/virtual memory pages to back them. To my knowledge, linux is fairly unique among unix implementations to fault during memory access rather than fail gracefully at malloc.

http://linuxdevcenter.com/pub/a/linux/2006/11/30/linux-out-of-memor...

It's possible to use unconventional methods to preallocate real memory from the heap, but there's the whole issue of OS memory overcommitting. When this happens, two instances of a process can use shared copy-on-write memory, but the OS has only reserved enough ram for one copy. In the event that one of the processes has to change a shared page, it is necessary to clone the page, but that can fail.


char a[]="This is a very long non-const test string..."; // global variable might initially be loaded into shared memory pages.
void f() {
a[0]++; // segfault?
}


I guess I kind of proved your point for you ;)

I wanted to emphasise that mathematical correct programming is possible, but it requires similar mathematical correctness from the OS/language in order to be effectively correct. At the very extreme, one might argue that our hardware itself is probabilistic in nature, but that still doesn't dismiss the mathematical correctness of a *software* system in principal.

Reply Parent Score: 3

RE[7]: Comment by stabbyjones
by f0dder on Sun 28th Oct 2012 16:09 in reply to "RE[6]: Comment by stabbyjones"
f0dder Member since:
2009-08-05

char a[]="This is a very long non-const test string..."; // global variable might initially be loaded into shared memory pages.
void f() {
a[0]++; // segfault?
}
TC++PL, 5.2.2: "The type of a string literal is 'array of the appropriate number of const characters'" and "A string literal can be assigned to a char*. This is allowed because in previous definitions of C and C++, the type of a string literal was char*. Allowing the assignment of a string literal to a char* ensures that millions of lines of C and C++ remain valid. It is, however, an error to try to modify a string literal through such a pointer."

So, undefined behavior in C++, segfault if your compiler puts string data in readonly memory (true for Intel's C++ compiler and GCC, but not MSVC).

EDIT: need more coffee - your code is OK since it copies the the string literal into the non-const 'a' char array and assigns a pointer to that, rather than directly to the string literal.

Edited 2012-10-28 16:16 UTC

Reply Parent Score: 2