Greetings! gcl/acl2 loads many modules into its data section,
relocates, flushes the cache, and then executes the module.
The CACHE_LINE granularity option to cacheflush appears to be broken,
at least on 060. The following two have been tested and fail, whereas
the third has been tested and passes:
#define CLEAR_CACHE_LINE_SIZE 32
#define CLEAR_CACHE do {void
*v=memory->cfd.cfd_start,*ve=v+memory->cfd.cfd_size; \
cacheflush(v,FLUSH_SCOPE_LINE,FLUSH_CACHE_BOTH,ve-v);\
} while(0)
#define CLEAR_CACHE_LINE_SIZE 32
#define CLEAR_CACHE do {void
*v=memory->cfd.cfd_start,*ve=v+memory->cfd.cfd_size; \
v=(void *)((unsigned long)v & ~(CLEAR_CACHE_LINE_SIZE -
1));\
cacheflush(v,FLUSH_SCOPE_LINE,FLUSH_CACHE_BOTH,ve-v);\
} while(0)
#define CLEAR_CACHE_LINE_SIZE 32
#define CLEAR_CACHE do {void
*v=memory->cfd.cfd_start,*ve=v+memory->cfd.cfd_size; \
v=(void *)((unsigned long)v & ~(CLEAR_CACHE_LINE_SIZE -
1));\
cacheflush(v,FLUSH_SCOPE_PAGE,FLUSH_CACHE_BOTH,ve-v);\
} while(0)
I haven't tried the remaining cache-line case of rounding ve up to the
nearest 32 byte boundary, but barring this, there appears to be an error
in the cacheflush kernel function.
Take care,
--
Camm Maguire [EMAIL PROTECTED]
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
