Re: [Mono-dev] CodeContacts open sourced

[Greg Young]

On Sunday, January 11, 2015, Michael Hutchinson mhu...@xamarin.com wrote:

 On 9 January 2015 at 16:32, Greg Young gregoryyou...@gmail.com
 javascript:; wrote:
  It's not source analysis it theorem proving think formal proving a la
 eiffel

 The Code Contracts tools analyze (and rewrite) compiled code, but
 there's no reason why equivalent source analysis tools couldn't use a
 theorem prover.


This is true it can work on any ast as of now it works on il. Previously it
worked wih output from spec# and was called boogie.


  It's a massive!!!  task (like 5-10 man years) to bring it in as you need
 to
  put contracts on all of the mono code
 
  This is part of why it has not done well for Microsoft is much of the
  framework lacks co tracts which makes the theorem prover very difficult
 to
  use (needs tons of assume clauses)

 The repo includes the contract annotations for the BCL, and we have
 the reference source for much of the BCL too.


Many of these are auto generated not manually written. They wrote a tool in
msr to try to extract them. This also brings up an interesting question if
mono intends to match every contract. It is also a higher level of coupling.

If I even use just a few libraries without contracts the contract prover is
very annoying to use think about a call stack

Call: check preconditions- post conditions - returns v1
Call: no contracts param v1 returns v2 -
Call param v2 (how do you check preconditions?)

This gets worse when mutations are involved.

A big part of the reason the contracts library has not taken off is that
huge portions of library code in the space doesn't have contracts
associated with them. Also given the massive amounts of mutations that are
happening good contracts are often hard to write. A good example of this
would be stream.position post conditions after operations on a stream. Why
it's a particularly nasty example is that much of the contract is relying
on lower level code and assumes.

Don't get me wrong I love the idea of contracts. I am just pointing out
that it's a massive amount of work to get contracts on vast portions of
monos code base. If it's not pervasive then no one will use the contract
proving as its really annoying.

Cheers,

Greg



 - m



-- 
Studying for the Turing test
___
Mono-devel-list mailing list
Mono-devel-list@lists.ximian.com
http://lists.ximian.com/mailman/listinfo/mono-devel-list

Re: [Mono-dev] Mono.Unix.Native

[Greg Young]

Oops read is failing as well.

Aside from having aligned buffer sizes do I need to do something like memalign?

Cheers,

Greg

On Mon, Jan 12, 2015 at 3:55 AM, Greg Young gregoryyou...@gmail.com wrote:
 I have been trying to use Syscalls a bit but am getting an exception I
 can't figure out why.

 Opening code throws no exceptions:
 var flags = OpenFlags.O_RDWR | OpenFlags.O_DIRECT |
 OpenFlags.O_CREAT;
 //var f = NativeConvert.FromOpenFlags(flags); not needed?
 var han = Syscall.open(path, flags, FilePermissions.S_IRWXU);
 if(han  0)
 throw new Win32Exception();

 var handle = new SafeFileHandle((IntPtr) han, true);
 if(handle.IsInvalid) throw new Exception(Invalid handle);
 return handle;

 Then I call write:

 fixed (byte* b = buffer)
 {
 long ret = 0;
  do {
 ret = Syscall.write
 (handle.DangerousGetHandle().ToInt32(), b ,count);
 } while (Mono.Unix.UnixMarshal.ShouldRetrySyscall ((int) 
 ret));
 if(ret == -1)
 Mono.Unix.UnixMarshal.ThrowExceptionForLastErrorIf
 ((int) ret);
 }

 I get an invalid parameter exception. Read seems to work following a
 similar pattern so not quite sure whats wrong.

 My writes are of size 4096. Perhaps the issue is needing to call
 memalign? I would expect reads to fail as well then though

 Cheers,

 Greg


 13) Test Error :
 EventStore.Core.Tests.TransactionLog.Unbuffered.UnbufferedTests.when_writing_then_seeking_exact_to_alignment_and_writing_again
System.ArgumentException : Invalid argument
    Mono.Unix.UnixIOException : Invalid argument [EINVAL].
   at Mono.Unix.UnixMarshal.ThrowExceptionForLastError () [0x0] in
 filename unknown:0
   at Mono.Unix.UnixMarshal.ThrowExceptionForLastErrorIf (Int32 retval)
 [0x0] in filename unknown:0
   at EventStore.Core.TransactionLog.Unbuffered.NativeFile.Write
 (Microsoft.Win32.SafeHandles.SafeFileHandle handle, System.Byte[]
 buffer, UInt32 count, System.Int32 written) [0x0] in filename
 unknown:0
   at 
 EventStore.Core.TransactionLog.Unbuffered.UnbufferedIOFileStream.InternalWrite
 (System.Byte[] buffer, UInt32 count) [0x0] in filename unknown:0
   at EventStore.Core.TransactionLog.Unbuffered.UnbufferedIOFileStream.Flush
 () [0x0] in filename unknown:0
   at EventStore.Core.TransactionLog.Unbuffered.UnbufferedIOFileStream.Dispose
 (Boolean disposing) [0x0] in filename unknown:0
   at System.IO.Stream.Close () [0x0] in filename unknown:0
   at System.IO.Stream.Dispose () [0x0] in filename unknown:0
   at 
 EventStore.Core.Tests.TransactionLog.Unbuffered.UnbufferedTests.when_writing_then_seeking_exact_to_alignment_and_writing_again
 () [0x0] in filename unknown:0
   at (wrapper managed-to-native)
 System.Reflection.MonoMethod:InternalInvoke
 (System.Reflection.MonoMethod,object,object[],System.Exception)
   at System.Reflection.MonoMethod.Invoke (System.Object obj,
 BindingFlags invokeAttr, System.Reflection.Binder binder,
 System.Object[] parameters, System.Globalization.CultureInfo culture)
 [0x0] in filename unknown:0
 --UnixIOException



 --
 Studying for the Turing test



-- 
Studying for the Turing test
___
Mono-devel-list mailing list
Mono-devel-list@lists.ximian.com
http://lists.ximian.com/mailman/listinfo/mono-devel-list

Re: [Mono-dev] Mono.Unix.Native

[Greg Young]

To answer my own question in case anyone runs into this.

Try this:

private byte* Align(IntPtr buf, uint alignTo)
{
//The buffer must originally be at least one alignment bigger!
var diff = alignTo - (buf.ToInt64() % alignTo);
var aligned = (IntPtr)(buf.ToInt64() + diff);
return (byte*) aligned;
}

On Mon, Jan 12, 2015 at 4:19 AM, Greg Young gregoryyou...@gmail.com wrote:
 Oops read is failing as well.

 Aside from having aligned buffer sizes do I need to do something like 
 memalign?

 Cheers,

 Greg

 On Mon, Jan 12, 2015 at 3:55 AM, Greg Young gregoryyou...@gmail.com wrote:
 I have been trying to use Syscalls a bit but am getting an exception I
 can't figure out why.

 Opening code throws no exceptions:
 var flags = OpenFlags.O_RDWR | OpenFlags.O_DIRECT |
 OpenFlags.O_CREAT;
 //var f = NativeConvert.FromOpenFlags(flags); not needed?
 var han = Syscall.open(path, flags, FilePermissions.S_IRWXU);
 if(han  0)
 throw new Win32Exception();

 var handle = new SafeFileHandle((IntPtr) han, true);
 if(handle.IsInvalid) throw new Exception(Invalid handle);
 return handle;

 Then I call write:

 fixed (byte* b = buffer)
 {
 long ret = 0;
  do {
 ret = Syscall.write
 (handle.DangerousGetHandle().ToInt32(), b ,count);
 } while (Mono.Unix.UnixMarshal.ShouldRetrySyscall ((int) 
 ret));
 if(ret == -1)
 Mono.Unix.UnixMarshal.ThrowExceptionForLastErrorIf
 ((int) ret);
 }

 I get an invalid parameter exception. Read seems to work following a
 similar pattern so not quite sure whats wrong.

 My writes are of size 4096. Perhaps the issue is needing to call
 memalign? I would expect reads to fail as well then though

 Cheers,

 Greg


 13) Test Error :
 EventStore.Core.Tests.TransactionLog.Unbuffered.UnbufferedTests.when_writing_then_seeking_exact_to_alignment_and_writing_again
System.ArgumentException : Invalid argument
    Mono.Unix.UnixIOException : Invalid argument [EINVAL].
   at Mono.Unix.UnixMarshal.ThrowExceptionForLastError () [0x0] in
 filename unknown:0
   at Mono.Unix.UnixMarshal.ThrowExceptionForLastErrorIf (Int32 retval)
 [0x0] in filename unknown:0
   at EventStore.Core.TransactionLog.Unbuffered.NativeFile.Write
 (Microsoft.Win32.SafeHandles.SafeFileHandle handle, System.Byte[]
 buffer, UInt32 count, System.Int32 written) [0x0] in filename
 unknown:0
   at 
 EventStore.Core.TransactionLog.Unbuffered.UnbufferedIOFileStream.InternalWrite
 (System.Byte[] buffer, UInt32 count) [0x0] in filename unknown:0
   at EventStore.Core.TransactionLog.Unbuffered.UnbufferedIOFileStream.Flush
 () [0x0] in filename unknown:0
   at EventStore.Core.TransactionLog.Unbuffered.UnbufferedIOFileStream.Dispose
 (Boolean disposing) [0x0] in filename unknown:0
   at System.IO.Stream.Close () [0x0] in filename unknown:0
   at System.IO.Stream.Dispose () [0x0] in filename unknown:0
   at 
 EventStore.Core.Tests.TransactionLog.Unbuffered.UnbufferedTests.when_writing_then_seeking_exact_to_alignment_and_writing_again
 () [0x0] in filename unknown:0
   at (wrapper managed-to-native)
 System.Reflection.MonoMethod:InternalInvoke
 (System.Reflection.MonoMethod,object,object[],System.Exception)
   at System.Reflection.MonoMethod.Invoke (System.Object obj,
 BindingFlags invokeAttr, System.Reflection.Binder binder,
 System.Object[] parameters, System.Globalization.CultureInfo culture)
 [0x0] in filename unknown:0
 --UnixIOException



 --
 Studying for the Turing test



 --
 Studying for the Turing test



-- 
Studying for the Turing test
___
Mono-devel-list mailing list
Mono-devel-list@lists.ximian.com
http://lists.ximian.com/mailman/listinfo/mono-devel-list

[Mono-dev] Mono.Unix.Native

[Greg Young]

I have been trying to use Syscalls a bit but am getting an exception I
can't figure out why.

Opening code throws no exceptions:
var flags = OpenFlags.O_RDWR | OpenFlags.O_DIRECT |
OpenFlags.O_CREAT;
//var f = NativeConvert.FromOpenFlags(flags); not needed?
var han = Syscall.open(path, flags, FilePermissions.S_IRWXU);
if(han  0)
throw new Win32Exception();

var handle = new SafeFileHandle((IntPtr) han, true);
if(handle.IsInvalid) throw new Exception(Invalid handle);
return handle;

Then I call write:

fixed (byte* b = buffer)
{
long ret = 0;
 do {
ret = Syscall.write
(handle.DangerousGetHandle().ToInt32(), b ,count);
} while (Mono.Unix.UnixMarshal.ShouldRetrySyscall ((int) ret));
if(ret == -1)
Mono.Unix.UnixMarshal.ThrowExceptionForLastErrorIf
((int) ret);
}

I get an invalid parameter exception. Read seems to work following a
similar pattern so not quite sure whats wrong.

My writes are of size 4096. Perhaps the issue is needing to call
memalign? I would expect reads to fail as well then though

Cheers,

Greg


13) Test Error :
EventStore.Core.Tests.TransactionLog.Unbuffered.UnbufferedTests.when_writing_then_seeking_exact_to_alignment_and_writing_again
   System.ArgumentException : Invalid argument
   Mono.Unix.UnixIOException : Invalid argument [EINVAL].
  at Mono.Unix.UnixMarshal.ThrowExceptionForLastError () [0x0] in
filename unknown:0
  at Mono.Unix.UnixMarshal.ThrowExceptionForLastErrorIf (Int32 retval)
[0x0] in filename unknown:0
  at EventStore.Core.TransactionLog.Unbuffered.NativeFile.Write
(Microsoft.Win32.SafeHandles.SafeFileHandle handle, System.Byte[]
buffer, UInt32 count, System.Int32 written) [0x0] in filename
unknown:0
  at 
EventStore.Core.TransactionLog.Unbuffered.UnbufferedIOFileStream.InternalWrite
(System.Byte[] buffer, UInt32 count) [0x0] in filename unknown:0
  at EventStore.Core.TransactionLog.Unbuffered.UnbufferedIOFileStream.Flush
() [0x0] in filename unknown:0
  at EventStore.Core.TransactionLog.Unbuffered.UnbufferedIOFileStream.Dispose
(Boolean disposing) [0x0] in filename unknown:0
  at System.IO.Stream.Close () [0x0] in filename unknown:0
  at System.IO.Stream.Dispose () [0x0] in filename unknown:0
  at 
EventStore.Core.Tests.TransactionLog.Unbuffered.UnbufferedTests.when_writing_then_seeking_exact_to_alignment_and_writing_again
() [0x0] in filename unknown:0
  at (wrapper managed-to-native)
System.Reflection.MonoMethod:InternalInvoke
(System.Reflection.MonoMethod,object,object[],System.Exception)
  at System.Reflection.MonoMethod.Invoke (System.Object obj,
BindingFlags invokeAttr, System.Reflection.Binder binder,
System.Object[] parameters, System.Globalization.CultureInfo culture)
[0x0] in filename unknown:0
--UnixIOException



-- 
Studying for the Turing test
___
Mono-devel-list mailing list
Mono-devel-list@lists.ximian.com
http://lists.ximian.com/mailman/listinfo/mono-devel-list