Re: [isabelle] I need a fixed mutable array



Hi Gottfried,

most assembly formalisation don’t represent memory as an array, but as a function from address to value (usually byte or word). With that, read is just function application, store is function update. These are easier to reason about than arrays.

There are existing large formalisations of x86 out there that you might want to look at. E.g. the Cambridge model in HOL4, which is close to what you’d do in Isabelle, or the model of Ben Pierce’s group in Coq.

Cheers,
Gerwin


On 18.06.2014, at 1:56 am, Gottfried Barrow <igbi at gmx.com> wrote:

> Hi,
>
> I did a few searches to find whether there are mutable arrays in Isabelle. It appears there's not, though I found a little info:
>
> https://groups.google.com/forum/?fromgroups#!searchin/fa.isabelle/mutable$20arrayshttps://groups.google.com/forum/?fromgroups#!searchin/fa.isabelle/mutable$20arrays
>
> I need to simulate the RAM of a cpu, and this is what I've done with a record and list:
>
> record 'a marray = MList :: "'a list"
>
> definition "array_size_512 = ( (| MList = replicate 0x100 (0::nat) |), 0x100::nat )"
>
> fun array_write :: "('a marray * nat) => nat => 'a => ('a marray * nat) option" where
>  "array_write (an_array, a_size) index data = (
>     if (index >= a_size) then None
>     else Some (an_array(| MList := (MList an_array)[index := data] |), a_size)
>  )"
>
> value "array_write array_size_512 3 1234"
> value "array_write array_size_512 0x100 1234"
>
> I'm wondering if there's a better way to do that. Better efficiency would be good, but efficiency in Isabelle is not of utmost concern, since it will hopefully represent what will be done in assembly language.
>
> I'm just getting started, but a partial record for a Intel 64-bit cpu might be something like this, where "Mem" is the fixed mutable array to represent RAM:
>
> record cpu64 =
>  Ax :: nat
>  Bx :: nat
>  Mem :: "nat list"
>
> definition cpu_mem256 :: "cpu64 * nat" where
>  "cpu_mem256 =
>  ( (| Ax = 0, Bx = 0, Mem = (replicate 0x100 (0::nat)) |), 0x100::nat )"
>
> fun mem_write :: "(cpu64 * nat) => nat => nat => (cpu64 * nat) option" where
>  "mem_write (cpu, memsize) addr data = (
>     if (addr >= memsize) then None
>     else Some (cpu(| Mem := (Mem cpu)[addr := data] |), memsize)
>  )"
>
> This is the beginning of an attempt to tie into the SIMD instruction sets of the AMD and Intel microprocessors. The SIMD instructions use 128-bit and 256-bit registers to do multiple operations at the same time. I include a lot of links below.
>
> Thanks,
> GB
>
> Wiki Pages
>
> http://en.wikipedia.org/wiki/Streaming_SIMD_Extensions
> http://en.wikipedia.org/wiki/SSE2
> http://en.wikipedia.org/wiki/SSE3
> http://en.wikipedia.org/wiki/SSSE3
> http://en.wikipedia.org/wiki/SSE4
> http://en.wikipedia.org/wiki/Advanced_Vector_Extensions
>
> INTEL
>
> http://www.intel.com/content/www/us/en/processors/architectures-software-developer-manuals.html
> https://software.intel.com/en-us/intel-isa-extensions
>
> AMD (See AMD64 Arch Programmer's Manuals under the manual heading)
>
> http://developer.amd.com/resources/documentation-articles/developer-guides-manuals/
>
> PRO ASSEMBLY LANGUAGE (chapter 17)
>
> http://www.wrox.com/WileyCDA/WroxTitle/Professional-Assembly-Language.productCd-0764579010,descCd-tableOfContents.html
>
> http://media.wiley.com/product_data/excerpt/10/07645790/0764579010-2.pdf
>
>
>
>
>
>
>
>


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.