[isabelle] I need a fixed mutable array



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











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